copy-paste assignment 2~5

assets/why3/eucl_div.mlw

@@ -0,0 +1,30 @@
+(* Euclidean division
+
+   1. Prove correctness of euclideian divison:
+     `division a b` returns an integer `q` such that
+      `a = bq+r` and `0 <= r < b` for some `r`.
+   
+     - You have to strengthen the loop invariant.
+*)
+
+module Division
+
+  use int.Int
+
+  (* IMPORTANT: DON'T MODIFY LINES EXCEPT `TODO`s OR YOU WILL GET ZERO POINTS *)
+  let division (a b: int) : int
+    requires { a >= 0 }
+    requires { b > 0 }
+    ensures  { exists r: int. a = b * result + r /\ 0 <= r < b }
+  =
+    let ref q = 0 in
+    let ref r = a in
+    while r >= b do
+      invariant { true (*TODO*) } 
+      variant { r }
+      q <- q + 1;
+      r <- r - b
+    done;
+    q
+
+end

assets/why3/ex1_eucl_div.mlw

@@ -1,34 +0,0 @@
-(* Euclidean division
-
-   1. Prove soundness, i.e. (division a b) returns an integer q such that
-      a = bq+r and 0 <= r < b for some r.
-      (You have to strengthen the precondition.)
-
-      Do you have to require b <> 0? Why?
-
-   2. Prove termination.
-      (You may have to strengthen the precondition even further.)
-*)
-
-module Division
-
-  use int.Int
-
-  let division (a b: int) : int
-    requires { a > 0 /\ b > 0 }
-    ensures  { exists r: int. a = b * result + r /\ 0 <= r < b }
-  =
-    let ref q = 0 in
-    let ref r = a in
-    while r >= b do
-      invariant { a = b * q + r /\ r >= 0 }
-      variant { r }
-      q <- q + 1;
-      r <- r - b
-    done;
-    q
-
-  let main () =
-    division 1000 42
-
-end

assets/why3/fact.mlw

@@ -1,23 +1,17 @@
 (* Two programs to compute the factorial
 
-   Note: function "fact" from module int.Fact (already imported)
-   can be used in specifications.
-
    Questions:
 
    1. In module FactRecursive:
 
-      a. Prove soundness of function fact_rec.
-
-      b. Prove its termination.
+      a. Implement the program that satisfies specification.
 
    2. In module FactLoop:
 
-      a. Prove soundness of function fact_loop.
+      a. Strengthen the invariant to prove correctness of the given implementation.
 
-      b. Prove its termination.
-
-      c. Change the code to use a for loop instead of a while loop.
+      b. Select a correct variant to prove the termination.
+     
 *)
 
 module FactRecursive
@@ -29,9 +23,9 @@ module FactRecursive
     requires { n >= 0 }
     ensures  { result = fact n }
     variant { n }
-  =
-    if n = 0 then 1 else n * fact_rec (n - 1)
-
+  = (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *) 
+    0 (*TODO*)
+    
 end
 
 module FactLoop
@@ -45,8 +39,10 @@ module FactLoop
   = let ref m = 0 in
     let ref r = 1 in
     while m < n do
-      invariant { 0 <= m <= n /\ r = fact m }
-      variant { n - m }
+      (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *) 
+      invariant { true (* TODO *) }
+      variant { n (* TODO *) }
+      (* IMPORTANT: DON'T MODIFY THE BELOW LINES *) 
       m <- m + 1;
       r <- r * m
     done;

assets/why3/max.mlw

@@ -0,0 +1,29 @@
+(* Max
+
+  Given an array `a` of natural numbers with length `n`, 
+  return the maximum element of the array.
+  
+  You should stengthen the loop invariant.
+  
+*)
+
+module Max
+
+  use int.Int
+  use ref.Ref
+  use array.Array
+
+  let max (a: array int) (n: int) : (max: int)
+    requires { n = length a }
+    requires { forall i. 0 <= i < n -> a[i] >= 0 }
+    ensures  { forall i. 0 <= i < n -> a[i] <= max }
+    ensures { exists i. 0 <= i < n -> a[i] = max }
+  = let ref max = 0 in
+    for i = 0 to n - 1 do
+      (* IMPORTANT: MODIFY ONLY THIS INVARIANT, OR YOU'LL GET ZERO POINTS *)
+      invariant { true (*TODO*) }
+      if max < a[i] then max <- a[i];
+    done;
+    max
+
+end

assets/why3/pascal.mlw

@@ -0,0 +1,32 @@
+module Pascal
+  use int.Int
+  use ref.Ref
+  use array.Array
+
+  (* HINT: https://en.wikipedia.org/wiki/Pascal%27s_triangle *)
+  (* You should understand the Pascal's triangle first to find good invariants *) 
+  let rec function comb (n k: int) : int
+    requires { 0 <= k <= n }
+    variant  { n }
+    ensures  { result >= 1 }
+  = if k = 0 || k = n then 1 else comb (n-1) k + comb (n-1) (k-1)
+
+  (* Insert appropriate invariants so that Why3 can verify this function. *)
+  let chooses (n : int) : array int
+    requires { n > 0 }
+    ensures  { forall i: int.
+      0 <= i < length result -> result[i] = comb n i }
+  =
+    let ref row = Array.make 1 1 in
+    for r = 1 to n do
+      invariant { length row = r }
+      invariant { true (*TODO*) }
+      let new_row = Array.make (r+1) 1 in
+      for c = 1 to r-1 do
+        invariant { true (*TODO*) }
+        new_row[c] <- row[c-1] + row[c]
+      done;
+      row <- new_row
+    done;
+    row
+end

assets/why3/two_way.mlw

@@ -1,22 +1,12 @@
 (* Two Way Sort
 
    The following program sorts an array of Boolean values, with False<True.
+   
+   E.g.
+     two_way_sorted [True; False; False; True; False]
+     = [False; False; False; True; True]
 
-   Questions:
-
-   1. Prove safety i.e. the absence of array access out of bounds.
-
-   2. Prove termination.
-
-   3. Prove that array a is sorted after execution of function two_way_sort
-      (using the predicate sorted that is provided).
-
-   4. Show that after execution the array contents is a permutation of its
-      initial contents. Use the library predicate "permut_all" to do so
-      (the corresponding module ArrayPermut is already imported).
-
-      You can refer to the contents of array a at the beginning of the
-      function with notation "a at Init".
+   - Strengthen the invariants to prove correctness.
 *)
 
 module TwoWaySort
@@ -34,15 +24,20 @@ module TwoWaySort
     forall i1 i2: int. 0 <= i1 <= i2 < a.length -> a[i1] << a[i2]
 
   let two_way_sort (a: array bool) : unit
-    ensures { true }
+    ensures { sorted a }
+    ensures { permut_all (old a) a }
   =
-    label Init in
     let ref i = 0 in
     let ref j = length a - 1 in
     while i < j do
-      invariant { forall i1: int. 0 <= i1 < i -> a[i1] = False }
-      invariant { forall i2: int. j < i2 < length a -> a[i2] = True }
       invariant { 0 <= i /\ j < length a }
+      (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
+      invariant { forall i1: int. 0 <= i1 < i 
+        -> true (* TODO *) }
+      invariant { forall i2: int. j < i2 < length a 
+        -> true (* TODO *) }
+      invariant { true (* TODO *) }
+      (* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
       variant { j - i }
       if not a[i] then
         incr i