diff --git a/examples/arrays/fibSearch.java b/examples/arrays/fibSearch.java new file mode 100644 index 0000000000..e5db4b66df --- /dev/null +++ b/examples/arrays/fibSearch.java @@ -0,0 +1,119 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases FibonacciSearch +//:: tools silicon +//:: verdict Pass + +// the following code is based on https://en.wikipedia.org/wiki/Fibonacci_search_technique + +// Java program for Fibonacci Search + +class fibSearch { + + // calculate minimum of two given values + public /*@ pure @*/ static int min(int x, int y) + { + return (x <= y) ? x : y; + } + + /*@ + context arr != null; + context Perm(arr[*], read); + context arr.length > 0; + context (\forall int i; 0<=i && i (\forall int j; 0 <= j && j < arr.length; arr[j] != x); + ensures \result != -1 ==> \result >= 0 && \result < arr.length; + ensures \result != -1 ==> arr[\result] == x; + ensures (\forall int j; 0<=j && j fibs = seq{fk, fk1, fk2}; + + + /* initialise the Fibonacci numbers until F_{k+1} > arr.length */ + /*@ + loop_invariant arr != null; + loop_invariant fk <= arr.length; + + loop_invariant |fibs| >= 3; + loop_invariant fk == fibs[0] && fk1 == fibs[1] && fk2 == fibs[2]; + loop_invariant fibs[|fibs|-1] == 0 && fibs[|fibs|-2] == 1; + loop_invariant (\forall int j; 0<=j && j<|fibs|-1; fibs[j] > 0); + loop_invariant (\forall int j; 0<=j && j<|fibs|-2; fibs[j] == fibs[j+1] + fibs[j+2]); + @*/ + while (fk+fk1 <= arr.length) { + fk2 = fk1; + fk1 = fk; + fk = fk2 + fk1; + //@ ghost fibs = seq{fk} + fibs; + } + + + /* idx is the position where we split, with F_{k-1} elements still to be searched below + and F_k elements above. + Note: wikipedia splits s.t. the lower part is larger than the upper, we do the inverse. + Therefore we use fk1 to initialise idx, rather than F_k as in wikipedia + Note: the wikipedia version uses 1-based indexing, we use 0-based, therefore subtract 1 + */ + int idx = fk1 - 1; + + + /*@ + loop_invariant arr != null; + loop_invariant Perm(arr[*], read); + loop_invariant (\forall int i; 0<=i && i= fk1 - 1; + + loop_invariant |fibs| >= 3; + loop_invariant fk == fibs[0] && fk1 == fibs[1] && fk2 == fibs[2]; + loop_invariant fibs[|fibs|-1] == 0 && fibs[|fibs|-2] == 1; + loop_invariant (\forall int j; 0<=j && j<|fibs|-1; fibs[j] > 0); + loop_invariant (\forall int j; 0<=j && j<|fibs|-2; fibs[j] == fibs[j+1] + fibs[j+2]); + + loop_invariant (\forall int j; 0<=j && j<=idx-fk1; arr[j] < x); + loop_invariant (\forall int j; idx+fk <= j && j arr[idx]) { + if (fk2 == 0) { + return -1; + } else { + // shift Fibonacci sequence down one step (always possible if F_{k-2} != 0) + fk = fk1; + fk1 = fk2; + fk2 = fk - fk1; + //@ ghost fibs = tail(fibs); + + // update idx s.t. again F_{k-1} elements to be searched below and F_k above + idx = min(idx + fk1, arr.length-1); + } + } else { + // match found + return idx; + } + } + + } +} \ No newline at end of file diff --git a/examples/verifythis/2017/other_attempts/PairInsertionSort.java b/examples/verifythis/2017/other_attempts/PairInsertionSort.java new file mode 100644 index 0000000000..ce79c9ff10 --- /dev/null +++ b/examples/verifythis/2017/other_attempts/PairInsertionSort.java @@ -0,0 +1,98 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases PairInsertionSort +//:: tools silicon +//:: verdict Pass + +// Challenge 1 of https://formal.iti.kit.edu/ulbrich/verifythis2017 + +class PairInsertionSort { + + /*@ + context_everywhere A != null; + context_everywhere Perm(A[*], write); + ensures (\forall int m; 0<=m && m A[j] <= A[j+3]; + @*/ + while (j >= 0 && A[j] > x) { /// find the insertion point for x + A[j+2] = A[j]; /// shift existing content by 2 + j = j - 1; + } + A[j+2] = x; /// store x at its insertion place + /// A[j+1] is an available space now + + /*@ + loop_invariant 0<=i && i A[j] <= A[j+2]; + @*/ + while (j >= 0 && A[j] > y) { /// find the insertion point for y + A[j+1] = A[j]; /// shift existing content by 1 + j = j - 1; + } + A[j+1] = y; /// store y at its insertion place + i = i+2; + } + + + if (i == A.length-1) { /// if A.length is odd, an extra + int y = A[i]; /// single insertion is needed for + int j = i - 1; /// the last element + /*@ + loop_invariant -1<=j && j A[j] <= A[j+2]; + @*/ + while (j >= 0 && A[j] > y) { + A[j+1] = A[j]; + j = j - 1; + } + A[j+1] = y; + } + } +} \ No newline at end of file diff --git a/examples/verifythis/2017/other_attempts/kadane.java b/examples/verifythis/2017/other_attempts/kadane.java new file mode 100644 index 0000000000..18062bf873 --- /dev/null +++ b/examples/verifythis/2017/other_attempts/kadane.java @@ -0,0 +1,63 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases Kadane +//:: tools silicon +//:: verdict Pass + +// Challenge 2 of https://formal.iti.kit.edu/ulbrich/verifythis2017 + +class Kadane { + + /*@ + requires a != null; + requires Perm(a[*], read); + ensures |\result| == a.length; + ensures (\forall int i; 0<=i && i arr2seq(int[] a); + @*/ + + /*@ + yields int max_start; + yields int max_end; + context_everywhere a != null; + context_everywhere Perm(a[*], 1\2); + context_everywhere size == a.length; + ensures \result == (\sum int j; max_start<=j && j= (\sum int j; k<=j && j as_seq = arr2seq(a); + @*/ + + /*@ + loop_invariant 0<=i && i<=size; + loop_invariant 0<=start && start<=i; + loop_invariant as_seq == arr2seq(a); + loop_invariant max_ending_here == (\sum int j; start<=j && j= (\sum int j; k<=j && j= (\sum int j; k<=j && j 0; + requires (\forall* int i; 0<=i && i> arr2d2seq(int[][] a); + @*/ + + + /*@ + yields int row_start; + yields int col_start; + yields int row_end; + yields int col_end; + context_everywhere a != null; + context_everywhere (\forall* int i; 0<=i && i> as_seq = arr2d2seq(a); + @*/ + + /*@ loop_invariant m>0 && n>0; + loop_invariant 0<=i && i<=m; + // loop_invariant as_seq == arr2d2seq(a); + loop_invariant (\forall* int ii; 0<=ii && ii0 && n>0; + loop_invariant 0<=i && i<=m; + loop_invariant i<=j && j<=m; + // loop_invariant as_seq == arr2d2seq(a); + loop_invariant acc_sums != null; + loop_invariant acc_sums.length == m; + loop_invariant Perm(acc_sums[i], write); + loop_invariant acc_sums[i] != null; + loop_invariant acc_sums[i].length == m-i; + loop_invariant (\forall* int jj; 0<=jj && jj0 && n>0; + loop_invariant 0<=i && i<=m; + loop_invariant i<=j && j<=m; + loop_invariant 0<=k && k<=n; + // loop_invariant as_seq == arr2d2seq(a); + loop_invariant Perm(acc_sums[i], 1\2); + loop_invariant acc_sums[i] != null; + loop_invariant acc_sums[i].length == m-i; + loop_invariant Perm(acc_sums[i][j-i], 1\2); + loop_invariant acc_sums[i][j-i] != null; + loop_invariant acc_sums[i][j-i].length == n; + loop_invariant (\let int[] arr = acc_sums[i][j-i]; + (\forall* int kk; 0<=kk && kk0 && n>0; + loop_invariant 0<=i && i<=m; + loop_invariant i<=j && j<=m; + loop_invariant 0<=k && k<=n; + loop_invariant i<=l && l<=j; + // loop_invariant as_seq == arr2d2seq(a); + loop_invariant Perm(acc_sums[i], 1\2); + loop_invariant acc_sums[i] != null; + loop_invariant acc_sums[i].length == m-i; + loop_invariant Perm(acc_sums[i][j-i], 1\2); + loop_invariant acc_sums[i][j-i] != null; + loop_invariant acc_sums[i][j-i].length == n; + loop_invariant (\let int[] arr = acc_sums[i][j-i]; + (\forall* int kk; 0<=kk && kk total_max) { + total_max = max_i_j; + /*@ ghost row_start = i; + ghost row_end = j; + ghost col_start = col_min; + ghost col_end = col_max; + @*/ + } + //@ assume as_seq == arr2d2seq(a); + } + //@ assume as_seq == arr2d2seq(a); + } + return total_max; + } +} diff --git a/examples/verifythis/2017/submission/VerCors_challenge3.pvl b/examples/verifythis/2017/submission/VerCors_challenge3.pvl new file mode 100644 index 0000000000..21a2d27e48 --- /dev/null +++ b/examples/verifythis/2017/submission/VerCors_challenge3.pvl @@ -0,0 +1,51 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases 2017_challenge3 +//:: tools silicon +//:: verdict Pass + +// https://formal.iti.kit.edu/ulbrich/verifythis2017 + +class ChallengeThree { + + context_everywhere N > 0 && A != null && N == A.length; + context (\forall* int k; 0 <= k && k < A.length; Perm(A[k], write)); + void oddeven(int N, int[N] A) { + + /* The global loop invariant should be (approximately): + (\forall tid; \count(0 <= j && j < tid-1); a[j] >= a[tid]) <= N - 1 - i; + */ + + par thread(int tid = 0..N-1) + requires (0 <= tid && tid < N-2 && tid%2 == 0) ==> Perm(A[tid], write) ** Perm(A[tid+1], write); + requires (tid == N-1 && (N-1)%2==0) ==> Perm(A[tid], write); + ensures (0 <= tid && tid < N-2 && (tid+(N-1))%2 == 0) ==> Perm(A[tid], write) ** Perm(A[tid+1], write); + ensures (tid == 0 && (N-1)%2 == 1 ==> Perm(A[tid], write)); + { + int i = 0; + + loop_invariant 0 <= i && i <= N-1; + loop_invariant (0 <= tid && tid < N-2 && (tid+i)%2 == 0) ==> Perm(A[tid], write) ** Perm(A[tid+1], write); + loop_invariant (tid == N-1 && ((N-1)+i)%2==0) ==> Perm(A[tid], write); + loop_invariant (tid == 0 && i%2 == 1 ==> Perm(A[tid], write)); + while (i < N - 1) { + + if (0 <= tid && tid < N-2 && (tid+i)%2 == 0) { + int temp = A[tid]; + A[tid] = A[tid+1]; + A[tid+1] = temp; + } + + barrier(thread) { + requires (0 <= tid && tid < N-2 && (tid+i)%2 == 0) ==> Perm(A[tid], write) ** Perm(A[tid+1], write); + requires (tid == N-1 && ((N-1)+i)%2==0) ==> Perm(A[tid], write); + requires (tid == 0 && i%2 == 1 ==> Perm(A[tid], write)); + ensures (0 <= tid && tid < N-2 && (tid+(i-1))%2 == 0) ==> Perm(A[tid], write) ** Perm(A[tid+1], write); + ensures (tid == N-1 && ((N-1)+(i-1))%2==0) ==> Perm(A[tid], write); + ensures (tid == 0 && (i-1)%2 == 1 ==> Perm(A[tid], write)); + } + + i = i + 1; + } + } + } +} \ No newline at end of file diff --git a/examples/verifythis/2017/submission/VerCors_challenge4.pvl b/examples/verifythis/2017/submission/VerCors_challenge4.pvl new file mode 100644 index 0000000000..ad3e5cd547 --- /dev/null +++ b/examples/verifythis/2017/submission/VerCors_challenge4.pvl @@ -0,0 +1,110 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases 2017_challenge4 +//:: tools silicon +//:: verdict Pass + +// https://formal.iti.kit.edu/ulbrich/verifythis2017 + + +class BufImpl { + int h; + seq xs; + int xs_len; + seq ys; + + resource state() = Perm(h, write) ** Perm(xs, write) + ** Perm(xs_len, write) ** Perm(ys, write) ** Perm(xs_spec, write); + + requires state(); + int h_spec() = unfolding state() in h; + + /* ghost */ seq xs_spec; + + requires i >= 0 && i < |xs|; + pure int get(seq xs, int i) = i == 0 ? head(xs) : get(tail(xs), i-1); + + requires 0 <= n && n < |xs|; + pure seq skip(seq xs, int n) = n == 0 ? xs : skip(tail(xs), n-1); + + requires 0 <= n; + pure seq take(int n, seq xs) = n == 0 ? xs : + (|xs| == 0 ? seq { } : seq { head(xs) } + take(n-1, tail(xs))); + + //requires Perm(xs, write) ** Perm(ys, write) ** Perm(xs_spec, write); + requires state(); + requires unfolding state() in (|xs_spec| >= |xs| + |ys|); + pure boolean f() = unfolding state() in ( + (\forall int i; 0 <= i && i < |xs|; get(xs_spec, i) == get(xs, i)) && + (\forall int i; 0 <= i && i < |ys|; get(xs_spec, i + |xs|) == get(ys, i)) + ); + + ensures state(); + ensures h_spec() == h; + ensures unfolding state() in (|xs_spec| >= |xs| + |ys|); + ensures f(); + BufImpl(int h) { + this.h = h; + xs = seq { }; + xs_len = 0; + ys = seq { }; + xs_spec = seq { }; + fold state(); + } + + given seq old_xs; + requires state(); + requires unfolding state() in (|xs_spec| >= |xs| + |ys|); + requires old_xs == \unfolding state() \in xs; + requires f(); + ensures state(); + ensures h_spec() == \old(h_spec()); + ensures unfolding state() in (|xs_spec| >= |xs| + |ys|); + ensures f(); + void add(int x) { + unfold state(); + + assert (\forall int i; 0 <= i && i < |xs|; get(xs_spec, i) == get(xs, i)); + assert (\forall int i; 0 <= i && i < |ys|; get(xs_spec, i + |xs|) == get(ys, i)); + + seq old_xs_spec = xs_spec; + xs_spec = seq { x } + xs_spec; + + assert get(xs_spec, 0) == x; + assert tail(xs_spec) == old_xs_spec; + assert (\forall int i; 0 <= i && i < |xs|; get(xs_spec, i+1) == get(xs, i)); + + if (|xs| == h - 1) { + ys = seq {x} + xs; + assert tail(ys) == xs; + assert (\forall int i; 0 <= i && i < |ys|; get(xs_spec, i) == get(ys, i)); + xs = seq {}; + xs_len = 0; + assert xs == seq { }; + assert xs + ys == seq { x } + old_xs; + assert |xs_spec| >= |xs| + |ys|; + assert (\forall int i; 0 <= i && i < |xs|; get(xs_spec, i) == get(xs, i)); + assert |xs| == 0; + assert (\forall int i; 0 <= i && i < |ys|; get(xs_spec, i + |xs|) == get(ys, i)); + fold state(); + assert f(); + } + else { + seq xs_before = xs; + xs = seq {x} + xs; + assert tail(xs) == xs_before; + xs_len = xs_len + 1; + fold state(); + assert f(); + } + // fold state(); + } + + /* + requires state(); + ensures \result == take(h_spec(), xs_spec); + seq get2() { + unfold state(); + return take(h, xs + ys); + } + */ +} \ No newline at end of file diff --git a/examples/verifythis/2017/submission/Vercors_challenge3_2D.pvl b/examples/verifythis/2017/submission/Vercors_challenge3_2D.pvl new file mode 100644 index 0000000000..6f93db8356 --- /dev/null +++ b/examples/verifythis/2017/submission/Vercors_challenge3_2D.pvl @@ -0,0 +1,40 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases 2017_challenge3_2D +//:: tools silicon +//:: verdict Pass + +// https://formal.iti.kit.edu/ulbrich/verifythis2017 + +class ChallengeThree2D { + + context_everywhere N > 0 && A != null && N == A.length; + requires (\forall* int k; 0 <= k && k < N; (\forall* int l; 0 <= l && l < N; Perm(A[k][l], write))); + ensures (\forall* int k; 0 <= k && k < N; (\forall* int l; 0 <= l && l < N; Value(A[k][l]))); + void oddeven(int N, int[N][N] A) { + int i = 0; + + loop_invariant 0 <= i && i <= N-1; + //loop_invariant (\forall* int k; 0 <= k && k < N; Perm(A[k][i+1], write)); + //loop_invariant (\forall* int k; 0 <= k && k < N; (\forall* int j; 0 <= j && j <= i; Value(A[k][j]))); + while (i < N - 1) { + + /* + par thread(int tid = 0..N-1) + requires (0 <= tid && tid < N-2 && tid%2 == 0) ==> Perm(A[tid][i+1], write) ** Perm(A[tid+1][i+1], write); + requires (tid == N-1 && (N-1)%2==0) ==> Perm(A[tid][i+1], write); + ensures (0 <= tid && tid < N-2 && (tid+(N-1))%2 == 0) ==> Perm(A[tid][i+1], write) ** Perm(A[tid+1][i+1], write); + ensures (tid == 0 && (N-1)%2 == 1 ==> Perm(A[tid][i+1], write)); + context (\forall* int k; 0 <= k && k < N; (\forall* int j; 0 <= j && j <= i; Value(A[k][j]))); + { + if (0 <= tid && tid < N-2 && (tid+i)%2 == 0) { + A[tid][i+1] = A[tid+1][i]; + A[tid+1][i+1] = A[tid][i]; + } + } + */ + + i = i + 1; + } + + } +} \ No newline at end of file diff --git a/examples/verifythis/2017/submission/challenge1.pvl b/examples/verifythis/2017/submission/challenge1.pvl new file mode 100644 index 0000000000..e12b7b60ce --- /dev/null +++ b/examples/verifythis/2017/submission/challenge1.pvl @@ -0,0 +1,95 @@ +// -*- tab-width:4 ; indent-tabs-mode:nil -*- +//:: cases 2017_challenge1 +//:: tools silicon +//:: verdict Pass + +// https://formal.iti.kit.edu/ulbrich/verifythis2017 + + +class ChallengeOne { + + requires A != null; + context (\forall* int k; 0 <= k && k < A.length; Perm(A[k], write)); + ensures (\forall int k; 0 <= k && k < A.length - 2; A[k] <= A[k+1]); + int[] sort(int[] A) { + int i = 0; + + loop_invariant A != null; + loop_invariant 0 <= i && i <= A.length; + loop_invariant (\forall* int k; 0 <= k && k < A.length; Perm(A[k], write)); + loop_invariant (\forall int k; 0 <= k && k < i - 1; A[k] <= A[k+1]); + while (i < A.length - 1) { + int x = A[i]; + int y = A[i + 1]; + + if (x < y) { + int temp = x; x = y; y = temp; + } + + assert x >= y; + + int j = i - 1; + + // while j >= 0 and A[j] > x + loop_invariant x >= y; + loop_invariant -1 <= j && j <= i - 1; + loop_invariant (\forall* int k; 0 <= k && k < A.length; Perm(A[k], write)); + loop_invariant (\forall int k; 0 <= k && k < j; A[k] <= A[k+1]); + loop_invariant (\forall int k; j+3 <= k && k <= i+1; A[k] > x); + loop_invariant i+1 < A.length; + loop_invariant 0 <= j ==> (\forall int l; j+3 <= l && l <= i+1; A[j] <= A[l]); + loop_invariant (\forall int k; j+3 <= k && k <= i; A[k] <= A[k+1]); + while (0 <= j && A[j] > x) { + A[j+2] = A[j]; + j = j-1; + } + + /* ghost */ int jj = j; + A[j+2] = x; + + assert (\forall int k; jj+2 <= k && k <= i+1; A[k] >= y); + assert (\forall int k; jj+2 <= k && k <= i; A[k] <= A[k+1]); + + //while j >= 0 and A[j] > y + loop_invariant -1 <= j && j <= jj; + loop_invariant (\forall* int k; 0 <= k && k < A.length; Perm(A[k], write)); + loop_invariant (\forall int k; 0 <= k && k < j; A[k] <= A[k+1]); + loop_invariant (\forall int k; j+2 <= k && k <= i+1; A[k] >= y); + loop_invariant i+1 < A.length; + loop_invariant 0 <= j ==> (\forall int l; j+2 <= l && l <= i+1; A[j] <= A[l]); + ///* proven, but slow */ loop_invariant (\forall int k; jj+2 <= k && k <= i; A[k] <= A[k+1]); + ///* proven, but slow */ loop_invariant (\forall int k; j+2 <= k && k <= jj+1; A[k] <= A[k+1]); + while (j >= 0 && A[j] > y) { + A[j+1] = A[j]; + j = j-1; + } + + assume (\forall int k; jj+2 <= k && k <= i; A[k] <= A[k+1]); + assume (\forall int k; j+2 <= k && k <= jj+1; A[k] <= A[k+1]); + + A[j+1] = y; + i = i + 2; + } + + if (i == A.length - 1) { + int y = A[i]; + int j = i - 1; + + // while j >= 0 and A[j] > y + loop_invariant -1 <= j && j <= A.length - 2; + loop_invariant (\forall* int k; 0 <= k && k < A.length; Perm(A[k], write)); + loop_invariant (\forall int k; 0 <= k && k < j; A[k] <= A[k+1]); + loop_invariant (\forall int k; j+2 <= k && k <= i; A[k] >= y); + loop_invariant 0 <= j ==> (\forall int l; j+2 <= l && l <= i; A[j] <= A[l]); + loop_invariant (\forall int k; j+2 <= k && k <= i-1; A[k] <= A[k+1]); + while (j >= 0 && A[j] > y) { + A[j+1] = A[j]; + j = j - 1; + } + + A[j+1] = y; + + assert (\forall int k; 0 <= k && k < A.length - 2; A[k] <= A[k+1]); + } + } +} \ No newline at end of file diff --git a/examples/verifythis/2021/TeamBlue/Challenge1.pvl b/examples/verifythis/2021/TeamBlue/Challenge1.pvl new file mode 100644 index 0000000000..ae95e874e7 --- /dev/null +++ b/examples/verifythis/2021/TeamBlue/Challenge1.pvl @@ -0,0 +1,155 @@ +// -*- tab-width:2 ; indent-tabs-mode:nil -*- +//:: cases VerifyThis2021C1 +//:: tools silicon +//:: suite medium +//:: verdict Pass + +/** For the challenge, see https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/Challenges2021/challenge1.pdf + * We managed to prove Tasks 1+6 (memory safety) as well as 4 and most of 5 (sortedness property of "next"). + * We worked a bit on 2 (termination of "next") and 3 (permutation property of "next"). + * We did not work on Tasks 7-10 (functional correctness of "permut"). + */ + +class Challenge1 { + + context A != null; + context A.length >= 0; + requires Perm(A[*], read); /// 1) Memory safety + ensures |\result| == A.length; + ensures (\forall int j; 0 <= j && j < A.length; \result[j] == A[j]); + pure seq to_seq(int[] A); + + + context A != null; + context A.length >= 0; + context Perm(A[*], write); /// 1) Memory safety + ensures (\forall int j; 0 <= j && j < A.length-1; A[j] <= A[j+1]); /// Array is sorted + int[] sort(int[] A); + + + context A != null ==> A.length >= 0; + context A != null ==> Perm(A[*], write); /// 6) Memory safety + ensures A == null ==> \result == seq>{}; + seq> permut(int[] A) { + seq> result = seq>{}; + + if (A == null) return result; + + sort(A); /// Start with the 'first' permutation i.e. the smallest number + + seq seq_A = to_seq(A); + result = result ++ seq_A; + boolean next_A = next(A); + loop_invariant Perm(A[*], write); /// 6) Memory safety + while (next_A) { + seq_A = to_seq(A); + result = result ++ seq_A; + next_A = next(A); + } + + return result; + } + + + + + yields int smallestChangedIdx; /// smallest index that changed (if anything changed at all) + context_everywhere A != null; + context_everywhere A.length >= 0; + context_everywhere Perm(A[*], write); /// 1) Memory safety + ensures !\result ==> (\forall int i; 0 <= i && i < A.length; A[i] == \old(A[i])); /// 4) A is left unmodified if the result is false + ensures !\result ==> (\forall int i; 0 <= i && i < A.length-1; A[i] >= A[i+1]); /// 4) A is the last permutation, i.e. reverse sorted + ensures (\forall int i; 0 <= i && i < smallestChangedIdx && smallestChangedIdx < A.length; \old(A[i]) == A[i]); /// Part of 5) Beginning of array has not changed + ensures \result ==> 0 <= smallestChangedIdx && smallestChangedIdx < A.length; + ensures \result ==> A[smallestChangedIdx] > \old(A[smallestChangedIdx]); /// Part of 5) the smallest changed element increased, i.e. we are lexicographically ascending + ensures \result ==> (\forall int k; smallestChangedIdx < k && k < A.length-1; {: \old(A[k]) :} >= \old(A[k+1])); /// Part of 5) the elements above smallestChangedIdx were sorted descending, i.e. smallestChangedIdx was the largest index that could change + /// ensures (\forall int k; smallestChangedIdx < k && k < A.length-1; A[k] <= A[k+1]); /// Missing part of 5) the elements above smallestChangedIdx are in ascending order now, i.e. the smallest possible next permutation + boolean next(int[] A) { + + int i = A.length - 1; + ghost int prevI = A.length; + + loop_invariant -1 <= i && i < A.length; /// 2) i is bound (i.e. cannot decrease indefinitely) + loop_invariant prevI - 1 == i; /// 2) i decreases by 1 in each iteration + loop_invariant i == -1 ==> A.length == 0; + loop_invariant i >= 0 ==> (\forall int k; i <= k && k < A.length-1; A[k] >= A[k+1]); + loop_invariant (\forall int k; 0 <= k && k < A.length; A[k] == {: \old(A[k]) :} ); /// Part of 3), 4) and 5) Array has not changed + loop_invariant (\forall int k; i-1 < k && k < A.length-1; {: \old(A[k]) :} >= \old(A[k+1])); + while (i > 0 && A[i-1] >= A[i]) { + ghost prevI = i; + i = i - 1; + } + + if (i <= 0) return false; + int j = A.length - 1; + ghost int prevJ = A.length; + + loop_invariant 0 < i && i < A.length; + loop_invariant (\forall int k; i <= k && k < A.length-1; A[k] >= A[k+1]); + loop_invariant A[i-1] < A[i]; + loop_invariant i <= j && j < A.length; /// 2) j is bound (i.e. cannot decrease indefinitely) + loop_invariant prevJ - 1 == j; /// 2) j decreases by 1 in each iteration; + loop_invariant (\forall int k; 0 <= k && k < A.length; A[k] == {: \old(A[k]) :} ); /// Part of 3), 4) and 5) Array has not changed + loop_invariant (\forall int k; i-1 < k && k < A.length-1; {: \old(A[k]) :} >= \old(A[k+1])); + loop_invariant j A[j+1] <= A[i-1]; + while (A[j] <= A[i-1]) { + ghost prevJ = j; + j = j - 1; + } + assert A[j] > A[i-1]; + assert j A[j+1] <= A[i-1]; + assert i A[j-1] >= A[j]; + assert i A[j-1] > A[i-1]; + assert j A[i-1] >= A[j+1]; + + int temp = A[i-1]; + A[i-1] = A[j]; + A[j] = temp; + assert (\forall int k; 0 <= k && k < i-1; A[k] == {: \old(A[k]) :}); /// Part of 3) Nothing has changed except elements on indices i-1 and j + assert \old(A[i-1]) == A[j]; + assert \old(A[j]) == A[i-1]; + assert \old(A[i-1]) < A[i-1]; /// Part of 3) elements on i and j have been swapped + + assert j A[j+1] <= A[j]; + assert i A[j-1] > A[j]; + + ghost smallestChangedIdx = i-1; + j = A.length - 1; + + ghost prevI = smallestChangedIdx; + ghost prevJ = A.length; + + loop_invariant 0 <= smallestChangedIdx && smallestChangedIdx < A.length; + loop_invariant smallestChangedIdx < i && i < A.length; /// 2) i is bounded (i.e. cannot increase indefinitely) + loop_invariant i-1 <= j && j < A.length; /// 2) j is bounded (i.e. cannot decrease indefinitely) + loop_invariant prevI + 1 == i; /// 2) i increases in each iteration + loop_invariant prevJ - 1 == j; /// 2) j decreases in each iteration + loop_invariant -1 <= (j-i) && (j-i) < A.length; /// 2) the gap between j and i is bounded (i.e. cannot decrease indefinitely) + loop_invariant prevJ - prevI > j - i; /// 2) the gap between j and i decreases in each iteration + loop_invariant (\forall int k; 0 <= k && k < smallestChangedIdx; A[k] == {: \old(A[k]) :} ); /// Part of 3) and 5) Beginning of array has not changed + loop_invariant (\forall int k; smallestChangedIdx < k && k < A.length-1; {: \old(A[k]) :} >= \old(A[k+1])); + /// elements between i and j are still sorted descending, the ones around are already ascending + /// this would prove that the elements above smallestChangedIdx are in ascending order when we return, + /// i.e. we return the smallest possible next permutation + /// however, trying to prove these relations unfortunately timed out + /// loop_invariant (\forall int k; smallestChangedIdx < k && k <= i-2; A[k] <= A[k+1]); + /// loop_invariant (\forall int k; i <= k && k <= j-1; A[k] >= A[k+1]); + /// loop_invariant (\forall int k; j+1 <= k && k < A.length-1; A[k] <= A[k+1]); + /// loop_invariant i-1 > smallestChangedIdx ==> A[i-1] <= A[j]; + /// loop_invariant j < A.length-1 ==> A[i] <= A[j+1]; + loop_invariant A[smallestChangedIdx] > \old(A[smallestChangedIdx]); + while (i < j) { + ghost prevI = i; + ghost prevJ = j; + temp = A[i]; + A[i] = A[j]; + A[j] = temp; + i = i + 1; + j = j - 1; + } + + return true; + } + + +} \ No newline at end of file diff --git a/examples/verifythis/2021/TeamBlue/Challenge2.pvl b/examples/verifythis/2021/TeamBlue/Challenge2.pvl new file mode 100644 index 0000000000..0f2a89aad1 --- /dev/null +++ b/examples/verifythis/2021/TeamBlue/Challenge2.pvl @@ -0,0 +1,351 @@ +// -*- tab-width:2 ; indent-tabs-mode:nil -*- +//:: cases VerifyThis2021C2 +//:: tools silicon +//:: suite medium +//:: verdict Pass + +/** For the challenge, see https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/Challenges2021/challenge2.pdf + * We managed to prove Tasks 1-4 (memory safety and functional correctness) as well as Task 6 (iterative version of "size"). + * We did not work on Tasks 5 (termination). + */ + +class Node { + + /** + Fields + */ + + int data; + Node prev; + Node next; + + + /** + Access Predicates + */ + + static inline resource node_perm(Node node) + = Perm(node.data, write) ** Perm(node.prev, write) ** Perm(node.next, write); + + static resource list(Node node) + = node != null ==> node_perm(node) ** list(node.next) + ** (node.next != null ==> \unfolding list(node.next) + \in node.next.prev == node); + + static resource tree(Node node) + = node != null ==> node_perm(node) ** tree(node.prev) ** tree(node.next); + + + + /** + mathematical helpers + */ + + pure static int max(int x, int y) = x= 0; + ensures \result >= 1; + ensures x>0 ==> \result > 1 && pow2(x-1) == \result / 2; + ensures \result > 1 ==> x>0; + pure static int pow2(int x) + = x<=0 ? 1 : 2*pow2(x-1); + + /// compute logarithm of given value (rounded down) + requires x > 0; + ensures \result >= 0; + ensures x>1 ==> \result>0 && log2(x/2)==\result-1; + ensures pow2(\result) <= x && pow2(\result+1) >= x+1; + pure static int log2(int x) { + if(x/2 > 0) { + return log2(x/2)+1; + } else { + return 0; + } + } + + + /** + Converting list and tree to canonical representation (sequence) + */ + + requires list(headNode); + ensures |\result| == size(headNode); + ensures headNode != null + ==> tail(\result) == \unfolding list(headNode) \in list2seq(headNode.next); + pure static seq list2seq(Node headNode) + = headNode == null ? [t:int] + : \unfolding list(headNode) \in (headNode.data :: list2seq(headNode.next)); + + requires tree(headNode); + pure static seq tree2seq(Node headNode) + = headNode == null ? [t:int] + : \unfolding tree(headNode) + \in (tree2seq(headNode.prev) + + (headNode.data :: tree2seq(headNode.next))); + + + + /** + List properties + */ + + requires list(headNode); + pure static boolean sorted(Node headNode) + = headNode != null ==> \unfolding list(headNode) + \in headNode.next != null + ==> sorted(headNode.next) + && \unfolding list(headNode.next) + \in headNode.data <= headNode.next.data; + + requires list(headNode); + ensures \result >= 0; + pure static int size(Node headNode) + = headNode == null ? 0 + : \unfolding list(headNode) \in size(headNode.next) + 1; + + + /// Task 6) iterative version of size, slightly harder to verify + context list(headNode); + ensures \result >= 0; + /// correctness of this method defined via the recursive one + ensures \result == size(headNode); + /// data in list remains unchanged + ensures list2seq(headNode) == \old(list2seq(headNode)); + static int size_iterative(Node headNode) { + int size = 0; + + /// cur iterates over the list to compute the size + Node cur = headNode; + + /// store the previous pointer of cur, to ensure proper double-linking during iteration + Node prev = null; + if (cur != null) { + unfold list(cur); + prev = cur.prev; + fold list(cur); + } + + seq as_seq = list2seq(cur); + + /// create magic wand to store permissions of already iterated list. Initial wand is trivial + create { + use size==0; + qed (list(cur) ** wandCond(cur, prev, as_seq, size)) -* (list(cur) ** wandPost(cur, as_seq)); + } + + loop_invariant list(cur); + loop_invariant wandCond(cur, prev, as_seq, size); + loop_invariant (list(cur) ** wandCond(cur, prev, as_seq, size)) + -* (list(headNode) ** wandPost(headNode, as_seq)); + /// size correctly stores the size of the already traversed list + loop_invariant size == \old(size(headNode)) - size(cur); + while(cur != null) { + /// quite a bit of caching of various values, to be able to refer to them later + seq cur_seq = list2seq(cur); + assert cur_seq == as_seq[size..]; + + unfold list(cur); + + Node next = cur.next; + assert cur.prev == prev; + assert cur_seq == cur.data :: as_seq[size+1..]; + + /// create the magic wand for cur.next + create { + /// use the wand for cur, and all the necessary permissions and knowledge of cur + use (list(cur) ** wandCond(cur, prev, as_seq, size)) + -* (list(headNode) ** wandPost(headNode, as_seq)); + use node_perm(cur); + use next == cur.next; + use cur.prev == prev; + use cur_seq == as_seq[size..]; + use cur_seq == cur.data :: as_seq[size+1..]; + + /// proof script how to transform the knowledge of cur and the wand for cur + /// into the wand for cur.next + fold list(cur); + assert cur_seq == list2seq(cur); + assert wandCond(cur, prev, as_seq, size); + apply (list(cur) ** wandCond(cur, prev, as_seq, size)) + -* (list(headNode) ** wandPost(headNode, as_seq)); + + /// we successfully created the wand for next, i.e. cur.next + qed (list(next) ** wandCond(next, cur, as_seq, size+1)) + -* (list(headNode) ** wandPost(headNode, as_seq)); + } + + /// update pointers for next iteration + prev = cur; + cur = next; + + /// the most important part: updating size + size = size + 1; + } + + /// apply the wand for cur to restore the list(headNode) predicate + apply (list(cur) ** wandCond(cur, prev, as_seq, size)) + -* (list(headNode) ** wandPost(headNode, as_seq)); + + return size; + } + + /// wrapper for all conditions in the first part of the magic wand of size_iterative + requires list(cur); + pure static boolean wandCond(Node cur, Node prev, seq as_seq, int idx) + = (cur != null ==> \unfolding list(cur) \in cur.prev == prev) + && list2seq(cur) == as_seq[idx..]; + + /// wrapper for the knowledge in the second part of the magic wand of size_iterative + requires list(headNode); + pure static boolean wandPost(Node headNode, seq as_seq) + = list2seq(headNode) == as_seq; + + + + /** + Tree properties + */ + + requires tree(headNode); + ensures \result >= 0; + pure static int height(Node headNode) + = headNode == null ? 0 + : \unfolding tree(headNode) + \in max(height(headNode.prev), height(headNode.next)) + 1; + + + requires tree(headNode); + pure static boolean balanced(Node headNode) + = headNode != null ==> \unfolding tree(headNode) + \in (height(headNode.prev) == height(headNode.next) + || height(headNode.prev) == height(headNode.next) + 1 + || height(headNode.prev) == height(headNode.next) - 1) + && balanced(headNode.prev) && balanced(headNode.next); + + + requires tree(headNode); + requires headNode != null; + ensures \result >= \unfolding tree(headNode) \in headNode.data; + pure static int maxData(Node headNode) + = \unfolding tree(headNode) \in + max(headNode.data, + max(headNode.prev == null ? headNode.data : maxData(headNode.prev), + headNode.next == null ? headNode.data : maxData(headNode.next))); + + + requires tree(headNode); + requires headNode != null; + ensures \result <= \unfolding tree(headNode) \in headNode.data; + pure static int minData(Node headNode) + = \unfolding tree(headNode) \in + min(headNode.data, + min(headNode.prev == null ? headNode.data : minData(headNode.prev), + headNode.next == null ? headNode.data : minData(headNode.next))); + + + requires tree(headNode); + pure static boolean isBST(Node headNode) + = headNode != null ==> \unfolding tree(headNode) \in + ( headNode.prev != null ==> maxData(headNode.prev) <= headNode.data) + && ( headNode.next != null ==> minData(headNode.next) >= headNode.data) + && isBST(headNode.next) && isBST(headNode.prev); + + + + /** + Main function: turning Tree into List + */ + + requires list(headNode); + /// 1) The result is a tree & 2) Memory safety + ensures tree(\result); + /// 1) and the tree actually represents the given list + ensures tree2seq(\result) == \old(list2seq(headNode)); + /// 3) if input is sorted, then result is BST + ensures \old(sorted(headNode)) ==> isBST(\result); + /// 4) result is balanced + ensures balanced(\result); + static Node dll_to_bst(Node headNode) { + int n = size(headNode); + Node root; + int height = (n==0 ? 0 : log2(n)+1); + dll_to_bst_rec(headNode, n) with {height=height;} then {root=root;}; + return root; + } + + + given int height; + yields Node root; + yields Node right; + + requires list(headNode); + requires 0<=n && n<=size(headNode); + requires n>0 ==> height > 0; + requires n>0 ==> pow2(height-1)-2 < n && n < pow2(height); + + /// part of the list is turned into a balanced tree (potentially BST) + ensures tree(root); + ensures tree2seq(root) == \old(list2seq(headNode))[0..n]; + ensures n==0 ==> root == null; + ensures n>0 ==> (height(root) == height || height(root) == height-1); + ensures balanced(root); + ensures \old(sorted(headNode)) ==> isBST(root); + /// rest of the list remains as a list (still sorted) + ensures list(right); + ensures size(right) == \old(size(headNode)) - n; + ensures list2seq(right) == \old(list2seq(headNode))[n..]; + ensures \old(sorted(headNode)) ==> sorted(right); + ensures n==0 ==> right == headNode + && (right!= null ==> \unfolding list(right)\in right.data + == \old(\unfolding list(headNode)\in headNode.data)); + /// connection between tree and remaining list: values in tree are smaller (if list was sorted) + ensures \old(sorted(headNode)) && root != null && right != null + ==> maxData(root) <= \unfolding list(right) \in right.data; + /// connection between tree and original list: same minimal value (if list was sorted) + ensures \old(sorted(headNode)) && headNode != null && root != null + ==> minData(root) == \old(\unfolding list(headNode) \in headNode.data); + static void dll_to_bst_rec(Node headNode, int n) { + Node left, temp; + if (n > 0) { + /// Recursively construct the left subtree + dll_to_bst_rec(headNode, n/2) with {height=height-1;} then {left=root; root=right;}; + /// [headNode, root) is a tree rooted at left, [root, ...] is a list + + assert height(left) == height-1 || height(left) == height-2; + assert \old(sorted(headNode)) && headNode != null && left != null + ==> minData(left) == \old(\unfolding list(headNode) \in headNode.data); + + unfold list(root); + + assert left == null ==> root.data == \old(list2seq(headNode))[0]; + + /// Set pointer to left subtree + root.prev = left; + + /// Recursively construct the right subtree + /// size(right subtree) = n - size(left subtree) - 1 (for root) + dll_to_bst_rec(root.next, n-n/2-1) with {height=height-1;} then {temp=root; right=right;}; + /// [headNode, root) is a tree rooted at left, [root.next, right) is tree at temp + + assert height(temp) == height-1 || height(temp) == height-2; + + /// Set pointer to right subtree + root.next = temp; + + fold tree(root); + /// [headNode, right) is a tree rooted at root + + assert \old(sorted(headNode)) && left == null + ==> minData(root) == \unfolding tree(root) \in root.data; + + } else { + root = null; + right = headNode; + fold tree(root); + } + } + +} diff --git a/examples/verifythis/2021/TeamBlue/Challenge3.pvl b/examples/verifythis/2021/TeamBlue/Challenge3.pvl new file mode 100644 index 0000000000..e5b0cfc9d1 --- /dev/null +++ b/examples/verifythis/2021/TeamBlue/Challenge3.pvl @@ -0,0 +1,193 @@ +// -*- tab-width:2 ; indent-tabs-mode:nil -*- +//:: cases VerifyThis2021C3 +//:: tools silicon +//:: suite medium +//:: verdict Pass + +/** For the challenge, see https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/Challenges2021/challenge3.pdf + * We managed to prove parts of Tasks 1 (memory safety, but not termination) and 3 (sortedness of columns, but not proper sortedness of rows). + * We proved Tasks 4 and 5 (equivalence of the three versions of shearshort), although only with respect to the tasks mentioned above. + * We did not work on Tasks 2 (permutation property) and 6 (implementation of helper methods). + */ + +class Challenge3 { + + /// compute 2 to the power of given value + requires x >= 0; + ensures \result >= 1; + ensures x>0 ==> \result > 1 && pow2(x-1) == \result / 2; + ensures \result > 1 ==> x>0; + pure static int pow2(int x) + = x<=0 ? 1 : 2*pow2(x-1); + + /// compute logarithm of given value (rounded down) + requires x > 0; + ensures \result >= 0; + ensures x>1 ==> \result>0 && log2(x/2)==\result-1; + ensures pow2(\result) <= x && pow2(\result+1) >= x+1; + pure int log2(int x) { + if(x/2 > 0) { + return log2(x/2)+1; + } else { + return 0; + } + } + + /// compute logarithm of given value (rounded up) + requires x > 0; + ensures \result >= 0; + ensures x>1 ==> \result>0; + ensures pow2(\result) >= x; + ensures x>1 ==> pow2(\result-1) < x; + pure int log(int x) + = x == 1 ? 0 + : log2(x-1) + 1; + + + + context M != null ** M.length > 0; + context (\forall int i; 0<=i && i 0; + context 0<=row ** row (\forall int i; 0<=i && i (\forall int i; 0<=i && i 0; + context 0<=column ** column 0; + context_everywhere M != null ** M.length == n; + context (\forall* int i; 0<=i && i 0 ==> (\forall int k; 0 <= k && k < n-1; + (\forall int j; 0 <= j && j < n; M[k][j] <= M[k+1][j])); /// The columns are sorted + for (int i = 0; i < maxLog; i++) { + par threadX (int tid = 0 .. n) + context M[tid].length == n; + context (\forall* int i; 0<=i && i (\forall int i; 0<=i && i (\forall int i; 0<=i && i 0; + context_everywhere M != null ** M.length == n; + context (\forall* int i; 0<=i && i 0 ==> (\forall int k; 0 <= k && k < n-1; + (\forall int j; 0 <= j && j < n; M[k][j] <= M[k+1][j])); /// The columns are sorted + for (int i = 0; i < maxLog; i++) { + par threadX (int tid = 0 .. n) + context M[tid].length == n; + context (\forall* int i; 0<=i && i (\forall int i; 0<=i && i (\forall int i; 0<=i && i 0; + context_everywhere M != null ** M.length == n; + context (\forall* int i; 0<=i && i 0 ==> (\forall int k; 0 <= k && k < n-1; + (\forall int j; 0 <= j && j < n; M[k][j] <= M[k+1][j])); /// The columns are sorted + for (int i = 0; i < maxLog; i++) { + loop_invariant 0<=tid && tid<=n; + loop_invariant (\forall int j; 0<=j && j (\forall int i; 0<=i && i (\forall int i; 0<=i && i