Add why3 files

assets/why3/ex4_two_way.mlw

@@ -0,0 +1,58 @@
+(* Two Way Sort
+
+   The following program sorts an array of Boolean values, with False<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".
+*)
+
+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 { true }
+  =
+    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 }
+      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