add settings, add recursive variant

KeYProject · Mar 26, 2024 · ef581da · ef581da
1 parent c3112b4
commit ef581da
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 1 deletion.
diff --git a/BinarySearch/prove.sh b/BinarySearch/prove.sh
@@ -3,6 +3,6 @@
 CI_TOOL=../tools/key-citool-1.6.0-mini.jar
 KEY=../tools/key-2.13.0-exe.jar
 
-java -cp $KEY:$CI_TOOL de.uka.ilkd.key.CheckerKt --proof-path proofs src/
+java -cp $KEY:$CI_TOOL de.uka.ilkd.key.CheckerKt --proof-path proofs project.key
 
 # project.key 2>&1 | tee prove.log
diff --git a/BinarySearch/src/BinSearch.java b/BinarySearch/src/BinSearch.java
@@ -31,4 +31,23 @@ private int binSearch(int v) {
 
     throw new RuntimeException();
   }
+
+  /*@ private normal_behavior
+    @   requires    0 <= low <= up <= a.length;
+    @   requires    (\forall int x, y; 0 <= x < y < a.length; a[x] <= a[y]);
+    @   ensures     \result == -1 || low <= \result < up;
+    @   ensures     (\exists int idx; low <= idx < up; a[idx] == v) ?
+    @                \result >= low && a[\result] == v : \result == -1;
+    @   assignable  \nothing;
+    @   measured_by up - low;
+    @*/
+  private int binSearchR(int v, int low, int up) {
+    if (low < up) {
+      int mid = low + ((up - low) / 2);
+      if (v == a[mid]) { return mid;
+      } else if (v < a[mid]) { return binSearchR(v, low, mid);
+      } else { return binSearchR(v, mid + 1, up); }
+    }
+    return -1;
+  }  
 }