## McCarthy's 91 function

Two different versions of McCarthy's 91 function:

• 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

```module McCarthy91

use int.Int

```

## Specification

```  function spec (x: int) : int = if x <= 100 then 91 else x-10

```

```  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 ref.Ref
use int.Iter

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 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 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

module McCarthyWithCoroutines

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 pc : ref int
val n : ref int
val e : ref int
val r : ref 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 aux1 () : 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 *)
aux1 ();
step (); (* 'if e=0' must be false *)
aux1 ()
end

let mccarthy1 ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 8 /\ !r = spec !n }
= step (); (* assignment e <- 1 *)
step (); (* assignment r <- n *)
aux1 (); (* 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 aux2 () : 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 aux2 (); next (); aux2 () end

let mccarthy2 ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 3 /\ !r = spec !n }
= next (); (* assignments e <- 1; r <- n *)
aux2 (); (* 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 e = ref one in
let n = ref 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 e = ref one 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 (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
```