Skip to content

Commit

Permalink
Fixed two invariants
Browse files Browse the repository at this point in the history
  • Loading branch information
unp1 committed Sep 10, 2024
1 parent 6a9eccd commit 52e780a
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 21 deletions.
5 changes: 2 additions & 3 deletions ArrayList/src/ArrayList.java
Original file line number Diff line number Diff line change
Expand Up @@ -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);
@*/
Expand Down
33 changes: 15 additions & 18 deletions BinarySearch/src/BinSearch.java
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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;
}
Expand Down

0 comments on commit 52e780a

Please sign in to comment.