From db7517ffb6bd5f60c39dd9ef8c89eb1f869dcf64 Mon Sep 17 00:00:00 2001
From: Jeehoon Kang <jeehoon.kang@kaist.ac.kr>
Date: Sat, 3 Sep 2022 23:10:14 +0900
Subject: [PATCH] Add why3 files

---
 assets/why3/binary_search.mlw | 23 ++++++++++++++
 assets/why3/ex1_eucl_div.mlw  | 34 ++++++++++++++++++++
 assets/why3/ex2_fact.mlw      | 55 +++++++++++++++++++++++++++++++++
 assets/why3/ex4_two_way.mlw   | 58 +++++++++++++++++++++++++++++++++++
 4 files changed, 170 insertions(+)
 create mode 100644 assets/why3/binary_search.mlw
 create mode 100644 assets/why3/ex1_eucl_div.mlw
 create mode 100644 assets/why3/ex2_fact.mlw
 create mode 100644 assets/why3/ex4_two_way.mlw

diff --git a/assets/why3/binary_search.mlw b/assets/why3/binary_search.mlw
new file mode 100644
index 0000000..d85c134
--- /dev/null
+++ b/assets/why3/binary_search.mlw
@@ -0,0 +1,23 @@
+(* Binary search
+
+   A classical example. Searches a sorted array for a given value v.
+   Consult <https://gitlab.inria.fr/why3/why3/-/blob/master/examples/binary_search.mlw>.
+ *)
+
+module BinarySearch
+
+  use import int.Int
+  use import int.ComputerDivision
+  use import ref.Ref
+  use import array.Array
+
+  let binary_search (a : array int) (v : int)
+    requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }
+    ensures  { 0 <= result <= length a }
+    ensures  { forall i: int. 0 <= i < result -> a[i] < v }
+    ensures  { result < length a -> a[result] >= v }
+  =
+    let l = ref (-1) in
+    let u = ref (length a) in
+    !u - !l (* TODO *)
+end
diff --git a/assets/why3/ex1_eucl_div.mlw b/assets/why3/ex1_eucl_div.mlw
new file mode 100644
index 0000000..00e7d58
--- /dev/null
+++ b/assets/why3/ex1_eucl_div.mlw
@@ -0,0 +1,34 @@
+(* 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
diff --git a/assets/why3/ex2_fact.mlw b/assets/why3/ex2_fact.mlw
new file mode 100644
index 0000000..343ae67
--- /dev/null
+++ b/assets/why3/ex2_fact.mlw
@@ -0,0 +1,55 @@
+(* 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.
+
+   2. In module FactLoop:
+
+      a. Prove soundness of function fact_loop.
+
+      b. Prove its termination.
+
+      c. Change the code to use a for loop instead of a while loop.
+*)
+
+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
diff --git a/assets/why3/ex4_two_way.mlw b/assets/why3/ex4_two_way.mlw
new file mode 100644
index 0000000..bfbe00e
--- /dev/null
+++ b/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