From 6cead8e79cf30df759456f2f41bf456fff801eeb Mon Sep 17 00:00:00 2001
From: Richard Bubel <bubel@cs.tu-darmstadt.de>
Date: Tue, 10 Sep 2024 16:46:42 +0200
Subject: [PATCH] fix for accidental modification

---
 BinarySearch/src/BinSearch.java | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/BinarySearch/src/BinSearch.java b/BinarySearch/src/BinSearch.java
index 07e208a..b36f919 100644
--- a/BinarySearch/src/BinSearch.java
+++ b/BinarySearch/src/BinSearch.java
@@ -6,13 +6,24 @@ class BinSearch {
     @   ensures    0 <= \result < a.length;
     @   ensures    a[\result] == v;
     @   assignable \nothing;
+    @ also 
+    @   private exceptional_behavior
+    @   requires   !(\exists int idx; 0 <= idx < a.length; a[idx] == v);
+    @   assignable \nothing;
+    @   signals_only RuntimeException;
     @*/
   private int binSearch(int[] a, int v) {
     int low = 0;
     int up = a.length;
   
+    /*@ loop_invariant 0 <= low <= up <= a.length;
+      @ loop_invariant (\forall int x; 0 <= x < low; a[x] != v);
+      @ loop_invariant (\forall int x; up <= x < a.length; a[x] != v);
+      @ assignable \nothing;
+      @ decreases up - low;
+      @*/
     while (low < up) {
-      int mid = (low + up) / 2;
+      int mid = low + ((up - low) / 2);
       if (v == a[mid]) { 
         return mid;
       } else if (v < a[mid]) {