gallery: yet another implementation of McCarthy's 91 function

this time with a manually-optimized tail call
(and auto-deref applied to all references in this file)
parent db8d11e1
...@@ -16,33 +16,45 @@ module McCarthy91 ...@@ -16,33 +16,45 @@ module McCarthy91
(** {2 traditional recursive implementation} *) (** {2 traditional recursive implementation} *)
let rec f91 (n:int) : int variant { 101-n } let rec f91 (n: int) : int
ensures { result = spec n } ensures { result = spec n } variant { 101 - n }
= if n <= 100 then = if n <= 100 then
f91 (f91 (n + 11)) f91 (f91 (n + 11))
else else
n - 10 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} *) (** {2 non-recursive implementation using a while loop} *)
use ref.Ref use ref.Ref
use int.Iter use int.Iter
let f91_nonrec (n0: int) ensures { result = spec n0 } let f91_nonrec (n0: int): int
= let e = ref 1 in ensures { result = spec n0 }
let n = ref n0 in = let ref e = 1 in
while !e > 0 do let ref n = n0 in
invariant { !e >= 0 /\ iter spec !e !n = spec n0 } while e > 0 do
variant { 101 - !n + 10 * !e, !e } invariant { e >= 0 /\ iter spec e n = spec n0 }
if !n > 100 then begin variant { 101 - n + 10 * e, e }
n := !n - 10; if n > 100 then begin
e := !e - 1 n <- n - 10;
e <- e - 1
end else begin end else begin
n := !n + 11; n <- n + 11;
e := !e + 1 e <- e + 1
end end
done; done;
!n n
(** {2 irrelevance of control flow} (** {2 irrelevance of control flow}
...@@ -54,33 +66,33 @@ module McCarthy91 ...@@ -54,33 +66,33 @@ module McCarthy91
exception Stop exception Stop
let f91_pseudorec (n0:int) : int let f91_pseudorec (n0: int) : int
ensures { result = spec n0 } ensures { result = spec n0 }
= let e = ref 1 in = let ref e = 1 in
let n = ref n0 in let ref n = n0 in
let bloc () : unit let bloc () : unit
requires { !e >= 0 } requires { e >= 0 }
ensures { !(old e) > 0 } ensures { (old e) > 0 }
ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1 ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
else !n = !(old n) + 11 /\ !e = !(old e) + 1 } else n = (old n) + 11 /\ e = (old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) } raises { Stop -> e = (old e) = 0 /\ n = (old n) }
= if not (!e > 0) then raise Stop; = if not (e > 0) then raise Stop;
if !n > 100 then begin if n > 100 then begin
n := !n - 10; n <- n - 10;
e := !e - 1 e <- e - 1
end else begin end else begin
n := !n + 11; n <- n + 11;
e := !e + 1 e <- e + 1
end end
in in
let rec aux () : unit let rec aux () : unit
requires { !e > 0 } requires { e > 0 }
variant { 101 - !n } variant { 101 - n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) } ensures { e = (old e) - 1 /\ n = spec (old n) }
raises { Stop -> false } raises { Stop -> false }
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd try aux (); bloc (); absurd
with Stop -> !n end with Stop -> n end
end end
...@@ -119,31 +131,31 @@ we define the small-step semantics of this code by the following [step] function ...@@ -119,31 +131,31 @@ we define the small-step semantics of this code by the following [step] function
*) *)
val pc : ref int val ref pc : int
val n : ref int val ref n : int
val e : ref int val ref e : int
val r : ref int val ref r : int
val step () : unit val step () : unit
requires { 0 <= !pc < 8 } requires { 0 <= pc < 8 }
writes { pc, e, r } writes { pc, e, r }
ensures { old !pc = 0 -> !pc = 1 /\ !e = 1 /\ !r = old !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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 6 -> pc = 7 /\ e = old e /\ r = old r + 11 }
ensures { old !pc = 7 -> !pc = 2 /\ !e = old !e + 1 /\ !r = old !r } ensures { old pc = 7 -> pc = 2 /\ e = old e + 1 /\ r = old r }
let rec monitor () : unit let rec monitor () : unit
requires { !pc = 2 /\ !e > 0 } requires { pc = 2 /\ e > 0 }
variant { 101 - !r } variant { 101 - r }
ensures { !pc = 5 /\ !r = spec(old !r) /\ !e = old !e - 1 } ensures { pc = 5 /\ r = spec(old r) /\ e = old e - 1 }
= step (); (* execution of 'if r > 100' *) = step (); (* execution of 'if r > 100' *)
if !pc = 3 then begin if pc = 3 then begin
step (); (* assignment r <- r - 10 *) step (); (* assignment r <- r - 10 *)
step (); (* assignment e <- e - 1 *) step (); (* assignment e <- e - 1 *)
end end
...@@ -156,8 +168,8 @@ we define the small-step semantics of this code by the following [step] function ...@@ -156,8 +168,8 @@ we define the small-step semantics of this code by the following [step] function
end end
let mccarthy () let mccarthy ()
requires { !pc = 0 /\ !n >= 0 } requires { pc = 0 /\ n >= 0 }
ensures { !pc = 8 /\ !r = spec !n } ensures { pc = 8 /\ r = spec n }
= step (); (* assignment e <- 1 *) = step (); (* assignment e <- 1 *)
step (); (* assignment r <- n *) step (); (* assignment r <- n *)
monitor (); (* loop *) monitor (); (* loop *)
...@@ -183,29 +195,29 @@ we define the not-so-small-step semantics of this code by the following [next] f ...@@ -183,29 +195,29 @@ we define the not-so-small-step semantics of this code by the following [next] f
*) *)
val next () : unit val next () : unit
requires { 0 <= !pc < 3 } requires { 0 <= pc < 3 }
writes { pc, e, r } writes { pc, e, r }
ensures { old !pc = 0 -> !pc = 1 /\ !e = 1 /\ !r = !n } ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = n }
ensures { old !pc = 1 /\ old !r > 100 -> ensures { old pc = 1 /\ old r > 100 ->
!pc = 2 /\ !r = old !r - 10 /\ !e = old !e - 1 } pc = 2 /\ r = old r - 10 /\ e = old e - 1 }
ensures { old !pc = 1 /\ old !r <= 100 -> ensures { old pc = 1 /\ old r <= 100 ->
!pc = 1 /\ !r = old !r + 11 /\ !e = old !e + 1 } 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 = 3 /\ r = old r /\ e = old e }
ensures { old !pc = 2 /\ old !e <> 0 -> !pc = 1 /\ !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 (* [aux2] performs as may loop iterations as needed so as to reach program point 2
from program point 1 *) from program point 1 *)
let rec monitor2 () : unit let rec monitor2 () : unit
requires { !pc = 1 /\ !e > 0 } requires { pc = 1 /\ e > 0 }
variant { 101 - !r } variant { 101 - r }
ensures { !pc = 2 /\ !r = spec(old !r) /\ !e = old !e - 1 } ensures { pc = 2 /\ r = spec(old r) /\ e = old e - 1 }
= next (); = next ();
if !pc <> 2 then begin monitor2 (); next (); monitor2 () end if pc <> 2 then begin monitor2 (); next (); monitor2 () end
let mccarthy2 () let mccarthy2 ()
requires { !pc = 0 /\ !n >= 0 } requires { pc = 0 /\ n >= 0 }
ensures { !pc = 3 /\ !r = spec !n } ensures { pc = 3 /\ r = spec n }
= next (); (* assignments e <- 1; r <- n *) = next (); (* assignments e <- 1; r <- n *)
monitor2 (); (* loop *) monitor2 (); (* loop *)
next () next ()
...@@ -233,49 +245,49 @@ module McCarthy91Mach ...@@ -233,49 +245,49 @@ module McCarthy91Mach
let f91_nonrec (n0: int63) : int63 let f91_nonrec (n0: int63) : int63
ensures { result = spec n0 } ensures { result = spec n0 }
= let e = ref one in = let ref e = one in
let n = ref n0 in let ref n = n0 in
while gt !e zero do while gt e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 } invariant { e >= 0 /\ iter spec e n = spec n0 }
variant { 101 - !n + 10 * !e, !e:int } variant { 101 - n + 10 * e, e:int }
if !n > 100 then begin if n > 100 then begin
n := !n - 10; n <- n - 10;
e := pred !e e <- pred e
end else begin end else begin
n := !n + 11; n <- n + 11;
e := succ !e e <- succ e
end end
done; done;
!n n
exception Stop exception Stop
let f91_pseudorec (n0: int63) : int63 let f91_pseudorec (n0: int63) : int63
ensures { result = spec n0 } ensures { result = spec n0 }
= let e = ref one in = let ref e = one in
let n = ref n0 in let ref n = n0 in
let bloc () : unit let bloc () : unit
requires { !e >= 0 } requires { e >= 0 }
ensures { !(old e) > 0 } ensures { (old e) > 0 }
ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1 ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
else !n = !(old n) + 11 /\ !e = !(old e) + 1 } else n = (old n) + 11 /\ e = (old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) } raises { Stop -> e = (old e) = 0 /\ n = (old n) }
= if not (gt !e zero) then raise Stop; = if not (gt e zero) then raise Stop;
if !n > 100 then begin if n > 100 then begin
n := !n - 10; n := n - 10;
e := pred !e e := pred e
end else begin end else begin
n := !n + 11; n := n + 11;
e := succ !e e := succ e
end end
in in
let rec aux () : unit let rec aux () : unit
requires { !e > 0 } requires { e > 0 }
variant { 101 - !n } variant { 101 - n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) } ensures { e = (old e) - 1 /\ n = spec (old n) }
raises { Stop -> false } raises { Stop -> false }
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd try aux (); bloc (); absurd
with Stop -> !n end with Stop -> n end
end end
...@@ -4,11 +4,39 @@ ...@@ -4,11 +4,39 @@
<why3session shape_version="5"> <why3session shape_version="5">
<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw" proved="true"> <file proved="true">
<path name=".."/>
<path name="mccarthy.mlw"/>
<theory name="McCarthy91" proved="true"> <theory name="McCarthy91" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true"> <goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="31"/></proof> <proof prover="3"><result status="valid" time="0.00" steps="31"/></proof>
</goal> </goal>
<goal name="VC f91_tco" expl="VC for f91_tco" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC f91_tco.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC f91_tco.1" expl="variant decrease" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC f91_tco.1.0" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC f91_tco.1.1" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_tco.2" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC f91_tco.3" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC f91_tco.4" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true"> <goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="3"><result status="valid" time="0.29" steps="523"/></proof> <proof prover="3"><result status="valid" time="0.29" steps="523"/></proof>
</goal> </goal>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment