assignment 1~5: fixes

- assignment05/pascal.mlw: lowered the difficulty (one more invariant given)
- assignment02, 03: minor fixes & divide into sub-problems

assets/why3/assignment05/binary_search.mlw

@@ -19,4 +19,4 @@ module BinarySearch
   =
     (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
     0 (* TODO *)
-end
+end

assets/why3/assignment05/max.mlw

@@ -4,7 +4,6 @@
   return the maximum element of the array.
   
   You should stengthen the loop invariant.
-  
 *)
 
 module Max
@@ -20,8 +19,9 @@ module 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*) }
+      (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
+      invariant { true (* TODO: Replace `true` with your solution *) }
+      (* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
       if max < a[i] then max <- a[i];
     done;
     max

assets/why3/assignment05/pascal.mlw

@@ -1,10 +1,14 @@
+(* Pascal
+
+  Prove that the Pascal's triangle indeed computes combinations.
+  HINT: https://en.wikipedia.org/wiki/Pascal%27s_triangle
+*)
+
 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 }
@@ -12,6 +16,7 @@ module Pascal
   = 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. *)
+  (* You SHOULD understand the Pascal's triangle first to find good invariants. *) 
   let chooses (n : int) : array int
     requires { n > 0 }
     ensures  { forall i: int.
@@ -20,10 +25,12 @@ module Pascal
     let ref row = Array.make 1 1 in
     for r = 1 to n do
       invariant { length row = r }
-      invariant { true (*TODO*) }
+      invariant { forall c: int. 0 <= c < r -> row[c] = comb (r-1) c } 
       let new_row = Array.make (r+1) 1 in
       for c = 1 to r-1 do
-        invariant { true (*TODO*) }
+        (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
+        invariant { true (* TODO: Replace `true` with your solution *) }
+        (* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
         new_row[c] <- row[c-1] + row[c]
       done;
       row <- new_row

assets/why3/exercises/ex1_eucl_div.mlw

@@ -11,7 +11,6 @@ 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 }
@@ -20,7 +19,7 @@ module Division
     let ref q = 0 in
     let ref r = a in
     while r >= b do
-      invariant { true (*TODO*) } 
+      invariant { true (* TODO: Replace `true` with your solution *) } 
       variant { r }
       q <- q + 1;
       r <- r - b

assets/why3/exercises/ex2_fact.mlw

@@ -39,10 +39,8 @@ module FactLoop
   = let ref m = 0 in
     let ref r = 1 in
     while m < n do
-      (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *) 
-      invariant { true (* TODO *) }
-      variant { n (* TODO *) }
-      (* IMPORTANT: DON'T MODIFY THE BELOW LINES *) 
+      invariant { true (* TODO: Replace `true` with your solution  *) }
+      variant { n (* TODO: Replace `n` with your solution  *) }
       m <- m + 1;
       r <- r * m
     done;

assets/why3/exercises/ex3_two_way.mlw

@@ -31,13 +31,11 @@ module TwoWaySort
     let ref j = length a - 1 in
     while i < j do
       invariant { 0 <= i /\ j < length a }
-      (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
       invariant { forall i1: int. 0 <= i1 < i 
-        -> true (* TODO *) }
+        -> true (* TODO: Replace `true` with your solution *) }
       invariant { forall i2: int. j < i2 < length a 
-        -> true (* TODO *) }
-      invariant { true (* TODO *) }
-      (* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
+        -> true (* TODO: Replace `true` with your solution *) }
+      invariant { true (* TODO: Replace `true` with your solution *) }
       variant { j - i }
       if not a[i] then
         incr i

assets/why3/exercises/solutions/ex1_eucl_div_sol.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 precondition.
+     - You have to strengthen the loop invariant.
+*)
+
+module Division
+
+  use int.Int
+
+  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 { a = b * q + r /\ 0 <= r } 
+      variant { r }
+      q <- q + 1;
+      r <- r - b
+    done;
+    q
+
+end

assets/why3/exercises/solutions/ex2_fact_sol.mlw

@@ -0,0 +1,37 @@
+(* Two programs to compute the factorial
+     
+*)
+
+module FactRecursive
+
+  use int.Int
+  use int.Fact
+
+  let rec fact_rec (n: int) : int
+    requires { n >= 0 }
+    ensures  { result = fact n }
+    variant { n }
+  =
+    if n = 0 then 1 else n * fact_rec (n - 1)
+
+end
+
+module FactLoop
+
+  use int.Int
+  use int.Fact
+
+  let fact_loop (n: int) : int
+    requires { 0 < n }
+    ensures  { result = fact n }
+  = let ref m = 0 in
+    let ref r = 1 in
+    while m < n do
+      invariant { 0 <= m <= n /\ r = fact m }
+      variant { n - m }
+      m <- m + 1;
+      r <- r * m
+    done;
+    r
+
+end

assets/why3/exercises/solutions/ex3_two_way_sol.mlw

@@ -0,0 +1,49 @@
+(* 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]
+
+   - Strengthen the invariant to prove correctness.
+*)
+
+module TwoWaySort
+
+  use int.Int
+  use bool.Bool
+  use ref.Refint
+  use array.Array
+  use array.ArraySwap
+  use array.ArrayPermut
+
+  predicate (<<) (x y: bool) = x = False \/ y = True
+
+  predicate sorted (a: array bool) =
+    forall i1 i2: int. 0 <= i1 <= i2 < a.length -> a[i1] << a[i2]
+
+  let two_way_sort (a: array bool) : unit
+    ensures { sorted a }
+    ensures { permut_all (old a) a }
+  =
+    let ref i = 0 in
+    let ref j = length a - 1 in
+    while i < j do
+      invariant { 0 <= i /\ j < length a }
+      invariant { forall i1: int. 0 <= i1 < i -> a[i1] = False }
+      invariant { forall i2: int. j < i2 < length a -> a[i2] = True }
+      invariant { permut_all (old a) a }
+      variant { j - i }
+      if not a[i] then
+        incr i
+      else if a[j] then
+        decr j
+      else begin
+        swap a i j;
+        incr i;
+        decr j
+      end
+    done
+
+end