Initial commit

README.md

@@ -0,0 +1,3 @@
+# whynot-research
+
+Tests in WhyML

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

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
+

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