## McCarthy's 91 function

Two different versions of McCarthy's 91 function:

• the traditional recursive implementation;
• a non-recursive implementation, using a while loop.
Both implementations are interesting examples of termination proofs.

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

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-loop
```
we 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