Skip to content

Commit

Permalink
Updates to tests corresponding to changes in OpenJML
Browse files Browse the repository at this point in the history
  • Loading branch information
davidcok committed Dec 13, 2024
1 parent 414690a commit 18708ef
Show file tree
Hide file tree
Showing 5 changed files with 6 additions and 7 deletions.
6 changes: 3 additions & 3 deletions examples/HeapSort.java
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ public class HeapSort {
ensures \forall int k;i <= k <= len/2;arr[k-1] <= arr[2*k-1];
ensures \forall int k;i <= k <= (len-1)/2;arr[k-1] <= arr[2*k];
@*/
public static void heapify(/*@ non_null @*/ int [] arr, final int i, final int len) {
public static void heapify(int /*@ non_null @*/ [] arr, final int i, final int len) {
int j = i;
/*@ loop_invariant i <= j <= len;
loop_invariant \forall int k; j < k <= len/2; arr[k-1] <= arr[2*k-1];
Expand Down Expand Up @@ -41,7 +41,7 @@ public static void heapify(/*@ non_null @*/ int [] arr, final int i, final int l
requires \forall int k; 1 <= k <= len/2; arr[k-1] <= arr[2*k-1];
requires \forall int k; 1 <= k <= (len-1)/2; arr[k-1] <= arr[2*k];
ensures \result && \forall int k; 0 < k < len; arr[k] >= arr[0]; //Always true
public static pure model boolean isGeq(final non_null int [] arr, final int len) {
public static pure model boolean isGeq(final int non_null [] arr, final int len) {
loop_invariant 0 <= i < len;
loop_invariant \forall int k;i < k < len;arr[k] >= arr[0];
decreasing i;
Expand All @@ -62,7 +62,7 @@ public static pure model boolean isGeq(final non_null int [] arr, final int le
/*@
ensures \forall int k,j; 0 <= k < j < arr.length; arr[k] >= arr[j];
@*/
public static void sort(/*@ non_null @*/ int [] arr) {
public static void sort(int /*@ non_null @*/ [] arr) {
// Array of size 1 is already sorted
if (arr.length < 2) return;

Expand Down
2 changes: 1 addition & 1 deletion examples/MergeSort.java
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ private static void sortRec(int [] arr, int l, int r) {
requires \forall int k,j; m <= k < j < r; arr[k] >= arr[j];
ensures \forall int k,j; l <= k < j < r; arr[k] >= arr[j] ;
@*/
private static void merge(/*@ non_null @*/ int [] arr, final int l, final int m, final int r) {
private static void merge(int /*@ non_null @*/ [] arr, final int l, final int m, final int r) {
final int [] lCpy = Arrays.copyOfRange(arr, l, m),
rCpy = Arrays.copyOfRange(arr,m, r);

Expand Down
2 changes: 1 addition & 1 deletion examples/SelectionSort.java
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ public class SelectionSort {
/*@
ensures \forall int k;0 <= k && k < arr.length-1;arr[k] >= arr[k+1];
@*/
public static void sort(/*@ non_null @*/ int [] arr) {
public static void sort(int /*@ non_null @*/ [] arr) {
//@ ghost final int n = arr.length;

//@ loop_invariant 0 <= i <= n; // Bounds check
Expand Down
2 changes: 1 addition & 1 deletion images/.gitignore
Original file line number Diff line number Diff line change
@@ -1 +1 @@
Thumbs.db
**/Thumbs.db
1 change: 0 additions & 1 deletion images/images/.gitignore

This file was deleted.

0 comments on commit 18708ef

Please sign in to comment.