diff --git a/examples/mccarthy.mlw b/examples/mccarthy.mlw index d8ec4f34e2a6c04e2e91759358d2dfca80a4a843..7dcc844cf74ac49d14ee796fc5ea9521df84b8f2 100644 --- a/examples/mccarthy.mlw +++ b/examples/mccarthy.mlw @@ -16,33 +16,45 @@ module McCarthy91 (** {2 traditional recursive implementation} *) - let rec f91 (n:int) : int variant { 101-n } - ensures { result = spec n } + 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) 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 + 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 + n <- n + 11; + e <- e + 1 end done; - !n + n (** {2 irrelevance of control flow} @@ -54,33 +66,33 @@ module McCarthy91 exception Stop - let f91_pseudorec (n0:int) : int + let f91_pseudorec (n0: int) : int ensures { result = spec n0 } - = let e = ref 1 in - let n = ref n0 in + = 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 + 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 + 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) } + 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 + = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in try aux (); bloc (); absurd - with Stop -> !n end + with Stop -> n end end @@ -119,31 +131,31 @@ 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 ref pc : int + val ref n : int + val ref e : int + val ref r : int val step () : unit - requires { 0 <= !pc < 8 } + 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 } + 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 } + 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 + if pc = 3 then begin step (); (* assignment r <- r - 10 *) step (); (* assignment e <- e - 1 *) end @@ -156,8 +168,8 @@ we define the small-step semantics of this code by the following [step] function end let mccarthy () - requires { !pc = 0 /\ !n >= 0 } - ensures { !pc = 8 /\ !r = spec !n } + requires { pc = 0 /\ n >= 0 } + ensures { pc = 8 /\ r = spec n } = step (); (* assignment e <- 1 *) step (); (* assignment r <- n *) monitor (); (* loop *) @@ -183,29 +195,29 @@ we define the not-so-small-step semantics of this code by the following [next] f *) val next () : unit - requires { 0 <= !pc < 3 } + 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 } + 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 } + 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 + if pc <> 2 then begin monitor2 (); next (); monitor2 () end let mccarthy2 () - requires { !pc = 0 /\ !n >= 0 } - ensures { !pc = 3 /\ !r = spec !n } + requires { pc = 0 /\ n >= 0 } + ensures { pc = 3 /\ r = spec n } = next (); (* assignments e <- 1; r <- n *) monitor2 (); (* loop *) next () @@ -233,49 +245,49 @@ module McCarthy91Mach 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 + = 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 + n <- n + 11; + e <- succ e end done; - !n + n exception Stop let f91_pseudorec (n0: int63) : int63 ensures { result = spec n0 } - = let e = ref one in - let n = ref n0 in + = 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 + 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 + 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) } + 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 + = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in try aux (); bloc (); absurd - with Stop -> !n end + with Stop -> n end end diff --git a/examples/mccarthy/why3session.xml b/examples/mccarthy/why3session.xml index 7c021e8f92f3b50c653e87933066e7478590aff4..b9cbfbcc4e0f757bc337e5790bbf0455cdb04a9e 100644 --- a/examples/mccarthy/why3session.xml +++ b/examples/mccarthy/why3session.xml @@ -4,11 +4,39 @@ <why3session shape_version="5"> <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"> +<file proved="true"> +<path name=".."/> +<path name="mccarthy.mlw"/> <theory name="McCarthy91" proved="true"> <goal name="VC f91" expl="VC for f91" proved="true"> <proof prover="3"><result status="valid" time="0.00" steps="31"/></proof> </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"> <proof prover="3"><result status="valid" time="0.29" steps="523"/></proof> </goal> diff --git a/examples/mccarthy/why3shapes.gz b/examples/mccarthy/why3shapes.gz index 733892f52f93a0175e1f33d84d811d691e72f6be..0e9d7e957abc66e8bd04ac36bfe9741b7a380954 100644 Binary files a/examples/mccarthy/why3shapes.gz and b/examples/mccarthy/why3shapes.gz differ