(** {1 McCarthy's "91" function} authors: Jean-Christophe FilliÃ¢tre, Martin Clochard, Claude MarchÃ© witness: Andrei Paskevich *) module McCarthy91 use int.Int (** {2 Specification} *) function spec (x: int) : int = if x <= 100 then 91 else x-10 (** {2 traditional recursive implementation} *) let rec f91 (n: int) : int ensures { result = spec n } variant { 101 - n } = if n <= 100 then f91 (f91 (n + 11)) else n - 10 (** {2 manually-optimized tail call} *) let rec f91_tco (n0: int) : int ensures { result = spec n0 } variant { 101 - n0 } = let ref n = n0 in while n <= 100 do invariant { n = n0 > 100 \/ n0 <= n <= 101 } variant { 101 - n } n <- f91_tco (n + 11) done; n - 10 (** {2 non-recursive implementation using a while loop} *) use ref.Ref use int.Iter let f91_nonrec (n0: int): int ensures { result = spec n0 } = let ref e = 1 in let ref n = n0 in while e > 0 do invariant { e >= 0 /\ iter spec 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 (** {2 irrelevance of control flow} We 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 ref e = 1 in let ref n = 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 module McCarthyWithGhostMonitor use int.Int use ref.Ref function spec (x: int) : int = if x <= 100 then 91 else x-10 (** {2 Variant using a general 'ghost coroutine' approach} Assume we want to prove the imperative code: {h
```e <- 1; r <- n;
loop
if r > 100 { r <- r - 10; e <- e - 1; if e = 0 break }
else { r <- r + 11; e <- e + 1 }
end-loop
```
} we annotate the various program points: {h
```{ 0 } e <- 1;
{ 1 } r <- n;
loop
{ 2 } if r > 100 then { 3 } r <- r - 10; { 4 } e <- e - 1; { 5 } if e=0 then break;
else { 6 } r <- r + 11; { 7 } e <- e + 1;
end-loop
{ 8 }
```
} we define the small-step semantics of this code by the following [step] function *) val ref pc : int val ref n : int val ref e : int val ref r : int val step () : unit requires { 0 <= pc < 8 } writes { pc, e, r } ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = old r } ensures { old pc = 1 -> pc = 2 /\ e = old e /\ r = n } ensures { old pc = 2 /\ old r > 100 -> pc = 3 /\ e = old e /\ r = old r } ensures { old pc = 2 /\ old r <= 100 -> pc = 6 /\ e = old e /\ r = old r } ensures { old pc = 3 -> pc = 4 /\ e = old e /\ r = old r - 10 } ensures { old pc = 4 -> pc = 5 /\ e = old e - 1 /\ r = old r } ensures { old pc = 5 /\ old e = 0 -> pc = 8 /\ e = old e /\ r = old r } ensures { old pc = 5 /\ old e <> 0 -> pc = 2 /\ e = old e /\ r = old r } ensures { old pc = 6 -> pc = 7 /\ e = old e /\ r = old r + 11 } ensures { old pc = 7 -> pc = 2 /\ e = old e + 1 /\ r = old r } let rec monitor () : unit requires { pc = 2 /\ e > 0 } variant { 101 - r } ensures { pc = 5 /\ r = spec(old r) /\ e = old e - 1 } = step (); (* execution of 'if r > 100' *) if pc = 3 then begin step (); (* assignment r <- r - 10 *) step (); (* assignment e <- e - 1 *) end else begin step (); (* assignment r <- r + 11 *) step (); (* assignment e <- e + 1 *) monitor (); step (); (* 'if e=0' must be false *) monitor () end let mccarthy () requires { pc = 0 /\ n >= 0 } ensures { pc = 8 /\ r = spec n } = step (); (* assignment e <- 1 *) step (); (* assignment r <- n *) monitor (); (* loop *) step() (* loop exit *) (** {2 a variant with not-so-small steps} we annotate the important program points: {h
```{ 0 } e <- 1;
r <- n;
loop
{ 1 }   if r > 100 { r <- r - 10; e <- e - 1; { 2 } if e = 0 break; }
else { r <- r + 11; e <- e + 1; }
end-loop
end-while
{ 3 }
return r
```
} we define the not-so-small-step semantics of this code by the following [next] function *) val next () : unit requires { 0 <= pc < 3 } writes { pc, e, r } ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = n } ensures { old pc = 1 /\ old r > 100 -> pc = 2 /\ r = old r - 10 /\ e = old e - 1 } ensures { old pc = 1 /\ old r <= 100 -> pc = 1 /\ r = old r + 11 /\ e = old e + 1 } ensures { old pc = 2 /\ old e = 0 -> pc = 3 /\ r = old r /\ e = old e } ensures { old pc = 2 /\ old e <> 0 -> pc = 1 /\ r = old r /\ e = old e } (* [aux2] performs as may loop iterations as needed so as to reach program point 2 from program point 1 *) let rec monitor2 () : unit requires { pc = 1 /\ e > 0 } variant { 101 - r } ensures { pc = 2 /\ r = spec(old r) /\ e = old e - 1 } = next (); if pc <> 2 then begin monitor2 (); next (); monitor2 () end let mccarthy2 () requires { pc = 0 /\ n >= 0 } ensures { pc = 3 /\ r = spec n } = next (); (* assignments e <- 1; r <- n *) monitor2 (); (* loop *) next () end module McCarthy91Mach use int.Int use mach.int.Int63 function spec (x: int) : int = if x <= 100 then 91 else x-10 let rec f91 (n: int63) : int63 variant { 101 - n } ensures { result = spec n } = if n <= 100 then f91 (f91 (n + 11)) else n - 10 use mach.peano.Peano use mach.int.Refint63 use int.Iter let f91_nonrec (n0: int63) : int63 ensures { result = spec n0 } = let ref e = one in let ref n = n0 in while gt e zero do invariant { e >= 0 /\ iter spec e n = spec n0 } variant { 101 - n + 10 * e, e:int } if n > 100 then begin n <- n - 10; e <- pred e end else begin n <- n + 11; e <- succ e end done; n exception Stop let f91_pseudorec (n0: int63) : int63 ensures { result = spec n0 } = let ref e = one in let ref n = 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 (gt e zero) then raise Stop; if n > 100 then begin n := n - 10; e := pred e end else begin n := n + 11; e := succ e 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