## 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. *) module McCarthy91 use import int.Int (* traditional recursive implementation *) let rec f91 (n:int) : int variant { 101-n } ensures { result = if n <= 100 then 91 else n - 10 } = if n <= 100 then f91 (f91 (n + 11)) else n - 10 (* non-recursive implementation using a while loop *) use import ref.Ref function f (x: int) : int = if x <= 100 then 91 else x-10 (* iter k x = f^k(x) *) clone import int.Iter with type t = int, function f = f let f91_nonrec (n0: int) ensures { result = f n0 } = let e = ref 1 in let n = ref n0 in while !e > 0 do invariant { !e >= 0 /\ iter !e !n = f 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 end

download ZIP archive