Commit dd3125e9 authored by François Bobot's avatar François Bobot

[Bench] mccarty f19_pseudorec is not proved

        without an additional assert and splitting. The splitting make
        also the bench faster by 2sec.
parent 28e84fe8
......@@ -82,10 +82,10 @@ valid_goals () {
test -d $1 || exit 1
for f in $1/*.mlw; do
printf " $f... "
if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
if ! $pgm -t 15 -P alt-ergo $2 $f > /dev/null 2>&1; then
echo "FAILED!"
echo "$pgm -t 15 -P alt-ergo $f"
$pgm -t 15 -P alt-ergo $f
echo "$pgm -t 15 -P alt-ergo $2 $f"
$pgm -t 15 -P alt-ergo $2 $f
exit 1
fi
echo "ok"
......@@ -308,6 +308,10 @@ echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking splitted valid goals ==="
valid_goals bench/valid/split_vc "-a split_vc"
echo ""
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
......
../../examples/mccarthy.mlw
\ No newline at end of file
(** {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 variant { 101-n }
ensures { result = spec n }
= if n <= 100 then
f91 (f91 (n + 11))
else
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
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 e = ref 1 in
let n = ref 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 McCarthyWithCoroutines
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 pc : ref int
val n : ref int
val e : ref int
val r : ref 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 aux1 () : 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 *)
aux1 ();
step (); (* 'if e=0' must be false *)
aux1 ()
end
let mccarthy1 ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 8 /\ !r = spec !n }
= step (); (* assignment e <- 1 *)
step (); (* assignment r <- n *)
aux1 (); (* 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 aux2 () : 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
let mccarthy2 ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 3 /\ !r = spec !n }
= next (); (* assignments e <- 1; r <- n *)
aux2 (); (* 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 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
end else begin
assert { spec !n = spec (spec (!n + 11)) };
n := !n + 11;
e := succ !e
end
done;
!n
exception Stop
let f91_pseudorec (n0: int63) : int63
ensures { result = spec n0 }
= let e = ref one in
let n = ref 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
......@@ -242,6 +242,7 @@ module McCarthy91Mach
n := !n - 10;
e := pred !e
end else begin
assert { spec !n = spec (spec (!n + 11)) };
n := !n + 11;
e := succ !e
end
......
......@@ -3,17 +3,18 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw" proved="true">
<theory name="McCarthy91" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00" steps="31"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="31"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.29" steps="517"/></proof>
<proof prover="1"><result status="valid" time="0.29" steps="517"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.01" steps="49"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
</theory>
<theory name="McCarthyWithCoroutines" proved="true">
......@@ -32,13 +33,41 @@
</theory>
<theory name="McCarthy91Mach" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="1067"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.07" steps="1067"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1"><result status="valid" time="6.06" steps="12891"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC f91_nonrec.0" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC f91_nonrec.1" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="26"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="32"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="200"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="100"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="34"/></proof>
</goal>
<goal name="VC f91_nonrec.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="274"/></proof>
</goal>
<goal name="VC f91_nonrec.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="432"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.08" steps="432"/></proof>
</goal>
</theory>
</file>
......
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