McCarthy's 91 function
Two different versions of McCarthy's 91 function:
- the traditional recursive implementation;
- a non-recursive implementation, using a while loop.
For the recursive implementation to be proved terminating, that is to prove that the variant 101-n decreases, we must actually establish a behavioral postcondition, which is here (n <= 100 and result = 91) or (n >= 101 and result = n - 10).
For the non-recursive implementation to be proved terminating, we need a lexicographic ordering.
Authors: Jean-Christophe Filliâtre
Topics: Tricky termination / Historical examples
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
McCarthy's "91" function
authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché witness: Andrei Paskevich
module McCarthy91 use int.Int
Specification
function spec (x: int) : int = if x <= 100 then 91 else x-10
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
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
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
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
Variant using a general 'ghost coroutine' approach
Assume we want to prove the imperative code:
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-loopwe annotate the various program points:
{ 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 *)
a variant with not-so-small steps
we annotate the important program points:
{ 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
download ZIP archive