Wiki Agenda Contact English version

McCarthy's 91 function

Two different versions of McCarthy's 91 function:

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.

Auteurs: Jean-Christophe Filliâtre

Catégories: Tricky termination / Historical examples

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