Merge pull request #697 from utwente-fmt/verifythis_examples

added examples from verifyThis competitions

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<arr.length; 
+                    (\forall int j; i<j && j<arr.length; arr[i] <= arr[j]));
+        ensures \result == -1 ==> (\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<arr.length; arr[j] == \old(arr[j]));
+    @*/
+    public static int fibonacciSearch(int[] arr, int x) {
+
+        // current Fibonacci number F_k, and the predecessing numbers F_{k-1} and F_{k-2}
+        int fk2 = 0;
+        int fk1 = 1;
+        int fk = fk1 + fk2;
+        //@ ghost seq<int> fibs = seq<int>{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<int>{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<arr.length; 
+                                (\forall int j; i<j && j<arr.length; arr[i] <= arr[j]));
+              loop_invariant (\forall int j; 0<=j && j<arr.length; arr[j] == \old(arr[j]));
+
+              loop_invariant 0<=idx && idx < arr.length;
+              loop_invariant idx >= 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.length; x < arr[j]);
+        @*/
+        while (true) {
+            if (x < arr[idx]) {
+                if (fk1 == 1) {
+                    return -1;
+                } else {
+                    // shift Fibonacci sequence down two steps (always possible if F_{k-1} != 1)
+                    fk = fk2;
+                    fk1 = fk1 - fk2;
+                    fk2 = fk - fk1;
+                    //@ ghost fibs = tail(tail(fibs));
+
+                    // update idx s.t. again F_k elements to be searched above and F_{k-1} below
+                    idx = idx - fk;
+                }
+            } else if (x > 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;
+            }
+        }
+
+    }
+}

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.length; 
+                    (\forall int k; m<k && k<A.length; A[m] <= A[k]));
+    @*/
+    public void sort(int[] A) {
+        int i = 0;                          /// i is running index (inc by 2 every iteration)
+
+        /*@ 
+            loop_invariant 0<=i && i<=A.length;
+            loop_invariant (\forall int m; 0<=m && m<i; 
+                                (\forall int k; m<k && k<i; A[m] <= A[k]));
+        @*/
+        while (i < A.length-1) {
+            int x = A[i];                   /// let x and y hold the next two elements in A
+            int y = A[i+1];
+            if (x < y) {
+                /// ensure that x is not smaller than y
+                int temp = x;
+                x = y;
+                y = temp;
+            }
+
+            int j = i - 1;                  /// j is the index used to find the insertion point
+            /*@ 
+                loop_invariant 0<=i && i<A.length-1;
+                loop_invariant -1<=j && j<i;
+                loop_invariant y <= x;
+                // loop_invariant (\forall int k; j<k && k<i; x<A[k+2]);
+                // same as above, but better for triggers
+                loop_invariant (\forall int k; j+2<k && k<i+2; x<A[k]);
+                loop_invariant (\forall int m; 0<=m && m<j; 
+                                    (\forall int k; m<k && k<=j; A[m] <= A[k]));
+                loop_invariant (\forall int m; j+3<=m && m<i+1; 
+                                    (\forall int k; m<k && k<=i+1; A[m] <= A[k]));
+                loop_invariant 0<=j && j<i-1 ==> 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.length-1;
+                loop_invariant -1<=j && j<i;
+                loop_invariant y <= A[j+2];
+                // loop_invariant (\forall int k; j<k && k<i; y<=A[k+1]);
+                // same as above, but better for triggers
+                loop_invariant (\forall int k; j+1<k && k<i+1; y<=A[k]);
+                loop_invariant (\forall int m; 0<=m && m<j; 
+                                    (\forall int k; m<k && k<=j; A[m] <= A[k]));
+                loop_invariant (\forall int m; j+2<=m && m<i+1; 
+                                    (\forall int k; m<k && k<=i+1; A[m] <= A[k]));
+                loop_invariant 0<=j && j<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.length-1;
+                // loop_invariant (\forall int k; j<k && k<i; y<=A[k+1]);
+                // same as above, but better for triggers
+                loop_invariant (\forall int k; j+1<k && k<i+1; y<=A[k]);
+                loop_invariant (\forall int m; 0<=m && m<j; 
+                                    (\forall int k; m<k && k<=j; A[m] <= A[k]));
+                loop_invariant (\forall int m; j+2<=m && m<A.length; 
+                                    (\forall int k; m<k && k<A.length; A[m] <= A[k]));
+                loop_invariant 0<=j && j<A.length-2 ==> A[j] <= A[j+2];
+            @*/
+            while (j >= 0 && A[j] > y) {
+                A[j+1] = A[j];
+                j = j - 1;
+            }
+            A[j+1] = y;
+        }
+    }
+}

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<a.length; \result[i] == a[i]);
+    static seq<int> 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<max_end; arr2seq(a)[j]);
+        ensures (\forall int k; 0<=k && k<=size; (\forall int m; k<=m && m<=size;
+                        \result >= (\sum int j; k<=j && j<m; arr2seq(a)[j])));
+    @*/
+    static int maxSubArraySum(int[] a, int size){
+        int max_so_far = 0, max_ending_here = 0;
+
+        /*@ ghost int start = 0; 
+            ghost max_start = 0;
+            ghost max_end = 0;
+            ghost seq<int> 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<i; as_seq[j]);
+            loop_invariant (\forall int k; 0<=k && k<=i; 
+                        max_ending_here >= (\sum int j; k<=j && j<i; as_seq[j]));
+            loop_invariant (\forall int k; 0<=k && k<=i; (\forall int m; k<=m && m<=i;
+                        max_so_far >= (\sum int j; k<=j && j<m; as_seq[j])));
+            loop_invariant max_so_far == (\sum int j; max_start<=j && j<max_end; as_seq[j]);
+        @*/
+        for (int i = 0; i < size; i++)
+        {
+            max_ending_here = max_ending_here + a[i];
+            if (max_ending_here < 0) {
+                max_ending_here = 0;
+                /*@ ghost start = i+1; @*/
+            } else if (max_so_far < max_ending_here) {
+                max_so_far = max_ending_here;
+                /*@ ghost max_start = start;
+                    ghost max_end = i+1; @*/
+            }
+        }
+        return max_so_far;
+    }
+
+}