mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
db9b0d9b78
this time with a manually-optimized tail call (and auto-deref applied to all references in this file)
294 lines
7.6 KiB
Plaintext
294 lines
7.6 KiB
Plaintext
|
|
(** {1 McCarthy's "91" function}
|
|
|
|
authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché
|
|
witness: Andrei Paskevich
|
|
|
|
*)
|
|
|
|
module McCarthy91
|
|
|
|
use int.Int
|
|
|
|
(** {2 Specification} *)
|
|
|
|
function spec (x: int) : int = if x <= 100 then 91 else x-10
|
|
|
|
(** {2 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
|
|
|
|
(** {2 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
|
|
|
|
(** {2 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
|
|
|
|
(** {2 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
|
|
|
|
(** {2 Variant using a general 'ghost coroutine' approach}
|
|
|
|
Assume we want to prove the imperative code:
|
|
{h <pre>
|
|
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
|
|
</pre>}
|
|
we annotate the various program points:
|
|
{h <pre>
|
|
{ 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 }
|
|
</pre>}
|
|
|
|
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 *)
|
|
|
|
(** {2 a variant with not-so-small steps}
|
|
|
|
we annotate the important program points:
|
|
{h <pre>
|
|
{ 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
|
|
</pre>}
|
|
|
|
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
|