(* McCarthy's ``91'' function. *) module McCarthy91 use import int.Int function spec (x: int) : int = if x <= 100 then 91 else x-10 (* traditional recursive implementation *) let rec f91 (n:int) : int variant { 101-n } ensures { result = spec n } = if n <= 100 then f91 (f91 (n + 11)) else n - 10 (* non-recursive implementation using a while loop *) use import ref.Ref (* iter k x = f^k(x) *) clone import int.Iter with type t = int, function f = spec let f91_nonrec (n0: int) ensures { result = spec n0 } = let e = ref 1 in let n = ref n0 in while !e > 0 do invariant { !e >= 0 /\ iter !e !n = spec n0 } variant { 101 - !n + 10 * !e, !e } if !n > 100 then begin n := !n - 10; e := !e - 1 end else begin n := !n + 11; e := !e + 1 end done; !n (* Use a 'morally' irrelevant control flow from a recursive function to ease proof (the recursive structure does not contribute to the program execution). This is a technique for proving derecursified programs. See verifythis_2016_tree_traversal for a more complex example. *) exception Stop let f91_pseudorec (n0:int) : int ensures { result = spec n0 } = let e = ref 1 in let n = ref n0 in let bloc () : unit requires { !e >= 0 } ensures { !(old e) > 0 } ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1 else !n = !(old n) + 11 /\ !e = !(old e) + 1 } raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) } = if not (!e > 0) then raise Stop; if !n > 100 then begin n := !n - 10; e := !e - 1 end else begin n := !n + 11; e := !e + 1 end in let rec aux () : unit requires { !e > 0 } variant { 101 - !n } ensures { !e = !(old e) - 1 /\ !n = spec !(old n) } raises { Stop -> false } = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in try aux (); bloc (); absurd with Stop -> !n end end