Commit 39fd4e82 authored by MARCHE Claude's avatar MARCHE Claude

example McCarthy: improve names

parent 8f539722
......@@ -85,7 +85,7 @@ module McCarthy91
end
module McCarthyWithCoroutines
module McCarthyWithGhostMonitor
use int.Int
......@@ -138,7 +138,7 @@ we define the small-step semantics of this code by the following [step] function
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
let rec monitor () : unit
requires { !pc = 2 /\ !e > 0 }
variant { 101 - !r }
ensures { !pc = 5 /\ !r = spec(old !r) /\ !e = old !e - 1 }
......@@ -150,17 +150,17 @@ we define the small-step semantics of this code by the following [step] function
else begin
step (); (* assignment r <- r + 11 *)
step (); (* assignment e <- e + 1 *)
aux1 ();
monitor ();
step (); (* 'if e=0' must be false *)
aux1 ()
monitor ()
end
let mccarthy1 ()
let mccarthy ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 8 /\ !r = spec !n }
= step (); (* assignment e <- 1 *)
step (); (* assignment r <- n *)
aux1 (); (* loop *)
monitor (); (* loop *)
step() (* loop exit *)
(** {2 a variant with not-so-small steps}
......@@ -195,19 +195,19 @@ we define the not-so-small-step semantics of this code by the following [next] f
(* [aux2] performs as may loop iterations as needed so as to reach program point 2
from program point 1 *)
let rec aux2 () : unit
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 aux2 (); next (); aux2 () end
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 *)
aux2 (); (* loop *)
monitor2 (); (* loop *)
next ()
end
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.5" 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"/>
<file name="../mccarthy.mlw" proved="true">
<theory name="McCarthy91" proved="true">
......@@ -16,18 +16,18 @@
<proof prover="3"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
</theory>
<theory name="McCarthyWithCoroutines" proved="true">
<goal name="VC aux1" expl="VC for aux1" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<theory name="McCarthyWithGhostMonitor" proved="true">
<goal name="VC monitor" expl="VC for monitor" proved="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC mccarthy1" expl="VC for mccarthy1" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<goal name="VC mccarthy" expl="VC for mccarthy" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC aux2" expl="VC for aux2" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<goal name="VC monitor2" expl="VC for monitor2" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mccarthy2" expl="VC for mccarthy2" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="McCarthy91Mach" proved="true">
......
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