From 15f3c791818b6ebd6035eacddf043ec86639bf04 Mon Sep 17 00:00:00 2001
From: Claudio Maggioni <maggicl@usi.ch>
Date: Mon, 17 Jul 2023 15:50:51 +0200
Subject: [PATCH] Initial commit

---
 README.md                |  3 +++
 whyml/gcd.why            | 50 ++++++++++++++++++++++++++++++++++++++++
 whyml/hello.why          | 10 ++++++++
 whyml/selection_sort.why | 27 ++++++++++++++++++++++
 4 files changed, 90 insertions(+)
 create mode 100644 README.md
 create mode 100644 whyml/gcd.why
 create mode 100644 whyml/hello.why
 create mode 100644 whyml/selection_sort.why

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..2dfa0a8
--- /dev/null
+++ b/README.md
@@ -0,0 +1,3 @@
+# whynot-research
+
+Tests in WhyML
diff --git a/whyml/gcd.why b/whyml/gcd.why
new file mode 100644
index 0000000..a434271
--- /dev/null
+++ b/whyml/gcd.why
@@ -0,0 +1,50 @@
+(*
+ * gcd.whyml
+ * WhyML implementation of byteback test `algorithm/GCD`
+ *)
+
+module GCD
+    use int.Int
+    use ref.Ref
+
+    exception IllegalArgumentException
+
+    let rec function gcd_recursive (a b : int) : int
+        variant { a + b }
+    =
+        if a = b then 
+            a
+        else if a > b then
+            gcd_recursive (a - b) b
+        else 
+            gcd_recursive a (b - a)
+
+    predicate arguments_are_negative (a b : int) =
+        a <= 0 || b <= 0
+
+    predicate result_is_gcd (a b r : int) =
+        (not (arguments_are_negative a b)) -> (r = gcd_recursive a b)
+        
+    let apply (a b : int) : int 
+        raises { IllegalArgumentException -> arguments_are_negative a b }
+        ensures { result_is_gcd a b result }
+        (* `result` holds return value *)
+    =
+        if a <= 0 || b <= 0 then
+            raise IllegalArgumentException;
+        let ref r: int = a in
+        let ref x: int = b in
+
+        while r <> x do 
+            invariant { r > 0 && x > 0 }
+            invariant { gcd_recursive r x = gcd_recursive a b }
+            variant { r + x } (* not needed for byteback *)
+            
+            if r > x then 
+                r <- r - x
+            else
+                x <- x - r;
+        done;
+
+        r
+end
diff --git a/whyml/hello.why b/whyml/hello.why
new file mode 100644
index 0000000..f60bff9
--- /dev/null
+++ b/whyml/hello.why
@@ -0,0 +1,10 @@
+theory HelloProof
+  goal G1: true
+  goal G4: false
+  goal G2: (true -> true) /\ (true \/ false)
+  use int.Int
+  goal G3: forall x:int. x * x >= 0
+
+  
+end
+
diff --git a/whyml/selection_sort.why b/whyml/selection_sort.why
new file mode 100644
index 0000000..1544291
--- /dev/null
+++ b/whyml/selection_sort.why
@@ -0,0 +1,27 @@
+module SelectionSort
+    use int.Int
+    use array.Array
+    use array.IntArraySorted
+    use array.ArraySwap
+    use array.ArrayPermut
+
+    let selection_sort (xs: array int)
+      ensures { sorted xs }
+      ensures { permut_all (old xs) xs } = 
+
+    let ref min = 0 in 
+    for i = 0 to length xs - 1 do
+      invariant { sorted_sub xs 0 i }
+      invariant { permut_all (old xs) xs }
+      invariant { forall k1 k2: int. 0 <= k1 < i <= k2 < length xs -> xs[k1] <= xs[k2] }
+        
+      min <- i;
+      for j = i + 1 to length xs - 1 do
+        invariant { i <= min < j }
+        invariant { forall k:int . i <= k < j -> xs[min] <= xs[k] }
+        
+        if xs[j] < xs[min] then min <- j
+      done;
+      swap xs min i;
+    done
+end