From 52e780acce8271bd1e549c7f9d475493a3168952 Mon Sep 17 00:00:00 2001
From: Richard Bubel <bubel@cs.tu-darmstadt.de>
Date: Tue, 10 Sep 2024 16:43:09 +0200
Subject: [PATCH] Fixed two invariants

---
 ArrayList/src/ArrayList.java    |  5 ++---
 BinarySearch/src/BinSearch.java | 33 +++++++++++++++------------------
 2 files changed, 17 insertions(+), 21 deletions(-)

diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
index a7bbe61..7c75044 100644
--- a/ArrayList/src/ArrayList.java
+++ b/ArrayList/src/ArrayList.java
@@ -3,13 +3,12 @@
 
 public class ArrayList implements List {
 
-    private /*@ nullable @*/ /*@ spec_public */ int[] array;
+    private /*@ spec_public */ int[] array;
     private int size = 0;
     
-    /*@ private invariant array != null;
+    /*@ 
       @ private invariant footprint == \set_union(array[*], this.*);
       @ private invariant 0 <= size && size <= array.length;
-      @ private invariant (\forall int i; 0 <= i && i < size; array[i] != null);
       @
       @ private invariant seq == \seq_sub(\array2seq(array), 0, size);
       @*/
diff --git a/BinarySearch/src/BinSearch.java b/BinarySearch/src/BinSearch.java
index 103b565..07e208a 100644
--- a/BinarySearch/src/BinSearch.java
+++ b/BinarySearch/src/BinSearch.java
@@ -6,27 +6,20 @@ 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 - low) / 2);
-      if (v == a[mid]) { return mid;
-      } else if (v < a[mid]) { up = mid;
-      } else { low = mid + 1; }
+      int mid = (low + up) / 2;
+      if (v == a[mid]) { 
+        return mid;
+      } else if (v < a[mid]) { 
+        up = mid;
+      } else { 
+        low = mid + 1; 
+      }
     }
   
     throw new RuntimeException();
@@ -44,9 +37,13 @@ private int binSearch(int[] a, int v) {
   private int binSearchR(int[] a, 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(a, v, low, mid);
-      } else { return binSearchR(a, v, mid + 1, up); }
+      if (v == a[mid]) { 
+        return mid;
+      } else if (v < a[mid]) { 
+        return binSearchR(a, v, low, mid);
+      } else { 
+        return binSearchR(a, v, mid + 1, up); 
+      }
     }
     return -1;
   }