Assignment 5 Done

assets/why3/assignment05/binary_search.mlw

@@ -18,6 +18,20 @@ module BinarySearch
     ensures  { forall i: int. result <= i < length a -> v <= a[i] }
   =
     (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
-    0 (* TODO *)
+    let ref l = 0 in
+    let ref r = length a in
+    while l < r do
+        invariant { 0 <= l <= length a /\ 0 <= r <= length a }
+        invariant { forall i: int. 0 <= i < l -> a[i] < v }
+        invariant { forall i: int. r <= i < length a -> a[i] >= v }
+        variant { r - l }
+        let m = l + div (r - l) 2 in
+        assert { l <= m < r };
+        if a[m] < v then
+            l := m + 1
+        else
+            r := m
+    done;
+    l
 
 end

assets/why3/assignment05/max.mlw

@@ -28,7 +28,7 @@ module Max
       invariant { 0 <= max_idx <= n-1 }
       (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
       (* TODO: Replace `true` with your solution. Your solution MUST be a single line, at line 31. DON'T add more code above or below. *)
-      invariant { true }
+      invariant { forall j. 0 <= j < i -> a[j] <= a[max_idx] }
       (* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
       if a[max_idx] < a[i] then max_idx <- i;
     done;

assets/why3/assignment05/pascal.mlw

@@ -33,7 +33,7 @@ module Pascal
       for c = 1 to r-1 do
         (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
         (* TODO: Replace `true` with your solution. Your solution MUST be a single line, at line 36. DON'T add more code above or below. *)
-        invariant { true  }
+        invariant { new_row[r] = comb r r /\ forall i: int. 0 <= i < c -> new_row[i] = comb r i }
         (* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
         new_row[c] <- row[c-1] + row[c]
       done;