factorial example

examples/programs/fact.mlw

+
+theory Fact "Factorial"
+
+  use export int.Int
+
+  logic fact int : int
+
+  axiom fact0: fact 0 = 1
+  axiom factn: forall n:int. n >= 1 -> fact n = fact (n-1) * n
+
+end
+
+
+module FactImperative
+
+use import Fact
+use import int.Int
+use import module ref.Ref
+
+let fact_imp (x:int) : int =
+  { x >= 0 }
+  let y = ref 0 in
+  let r = ref 1 in
+  while !y < x do 
+    invariant { 0 <= !y <= x and !r = fact !y }
+    y := !y + 1;
+    r := !r * !y
+  done; 
+  !r
+  { result = fact x }
+
+end