mlcfg: new examples

parent ebd799a0
module Fib
use int.Int
use int.Fibonacci
let cfg fib (n: int) : int
requires { n >= 0 }
ensures { result = fib n }
= var x: int;
var y: int;
var i: int;
{
x <- 0;
y <- 1;
i <- 0;
goto L1
}
L1 {
invariant I1 { 0 <= i <= n };
invariant I2 { x = fib i /\ y = fib (i + 1) };
switch (i = n)
| True -> x
| False -> y <- x + y; x <- y - x; i <- i + 1; goto L1
end
}
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="2" name="Alt-Ergo" version="2.3.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="arith.mlcfg"/>
<theory name="Fib" proved="true">
<goal name="fib&#39;vc" expl="VC for fib" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
</theory>
</file>
</why3session>
module BreakContinue
use int.Int
use int.ComputerDivision
(* translation of
x, i <- 0, 0;
while true do
if x > 20 then break;
i <- i + 1;
if i mod 2 = 0 then continue;
x <- x + i
done;
x
*)
let cfg example () : int
ensures { result = 25 }
= var x: int;
var i: int;
{
x <- 0;
i <- 0;
goto Loop
}
Loop {
invariant I1 { 0 <= i <= 9 };
invariant I2 { 4 * x = if mod i 2 = 0 then i * i else (i + 1) * (i + 1) };
switch (x > 20)
| True -> goto Break
| False -> goto L1
end
}
L1 {
i <- i + 1;
switch (mod i 2 = 0)
| True -> goto Loop (* continue *)
| False -> x <- x + i; goto Loop
end
}
Break {
x
}
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="2" name="Alt-Ergo" version="2.3.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="break_continue.mlcfg"/>
<theory name="BreakContinue" proved="true">
<goal name="example&#39;vc" expl="VC for example" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="51"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -6,8 +6,9 @@ module MaxArray
use array.Array
let cfg compute_max (a:array int) : (max: int, ghost ind:int)
requires { a.length > 0 }
ensures { forall i. 0 <= i < a.length -> a[ind] >= a[i] }
requires { length a > 0 }
ensures { 0 <= ind < length a }
ensures { forall i. 0 <= i < length a -> a[ind] >= a[i] }
=
(* simulation of the C code: (from ACSL Manual, section 2.4.2 Loop invariants)
......@@ -24,35 +25,34 @@ module MaxArray
return m;
*)
var i m:int;
ghost var ind:int;
var i m: int;
ghost var ind: int;
{
i <- 0;
goto L
i <- 0;
goto L
}
L {
m <- a[i];
ind <- i;
goto L1
}
}
L1 {
invariant i_bounds { 0 <= i < a.length };
invariant ind_bounds { 0 <= ind < a.length };
invariant i_bounds { 0 <= i < length a };
invariant ind_bounds { 0 <= ind < length a };
invariant m_and_ind { m = a[ind] };
invariant m_is_max { forall j. 0 <= j <= i -> m >= a[j] };
(* (yes, j <= i, not j < i !) *)
i <- i+1;
switch (i < a.length)
| True -> goto L2
| False -> (m,ind)
i <- i + 1;
switch (i < length a)
| True -> goto L2
| False -> (m, ind)
end
}
}
L2 {
switch (a[i] > m)
| True -> goto L
| True -> goto L
| False -> goto L1
end
}
}
end
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.3.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="max_array.mlcfg"/>
......@@ -24,49 +25,64 @@
<proof prover="2"><result status="valid" time="0.02" steps="2653"/></proof>
</goal>
<goal name="compute_max&#39;vc.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3038"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="2563"/></proof>
</goal>
<goal name="compute_max&#39;vc.6" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3018"/></proof>
<goal name="compute_max&#39;vc.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
<goal name="compute_max&#39;vc.7" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3018"/></proof>
</goal>
<goal name="compute_max&#39;vc.8" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3061"/></proof>
</goal>
<goal name="compute_max&#39;vc.8" expl="check" proved="true">
<goal name="compute_max&#39;vc.9" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3097"/></proof>
</goal>
<goal name="compute_max&#39;vc.9" expl="check" proved="true">
<goal name="compute_max&#39;vc.10" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3098"/></proof>
</goal>
<goal name="compute_max&#39;vc.10" expl="check" proved="true">
<goal name="compute_max&#39;vc.11" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="2549"/></proof>
</goal>
<goal name="compute_max&#39;vc.11" expl="check" proved="true">
<goal name="compute_max&#39;vc.12" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3448"/></proof>
</goal>
<goal name="compute_max&#39;vc.12" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3692"/></proof>
<goal name="compute_max&#39;vc.13" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2777"/></proof>
</goal>
<goal name="compute_max&#39;vc.14" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="compute_max&#39;vc.13" expl="check" proved="true">
<goal name="compute_max&#39;vc.15" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3072"/></proof>
</goal>
<goal name="compute_max&#39;vc.14" expl="check" proved="true">
<goal name="compute_max&#39;vc.16" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="2611"/></proof>
</goal>
<goal name="compute_max&#39;vc.15" expl="check" proved="true">
<goal name="compute_max&#39;vc.17" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2482"/></proof>
</goal>
<goal name="compute_max&#39;vc.16" expl="check" proved="true">
<goal name="compute_max&#39;vc.18" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3386"/></proof>
</goal>
<goal name="compute_max&#39;vc.17" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3648"/></proof>
<goal name="compute_max&#39;vc.19" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2770"/></proof>
</goal>
<goal name="compute_max&#39;vc.18" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3273"/></proof>
<goal name="compute_max&#39;vc.20" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="compute_max&#39;vc.19" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2965"/></proof>
<goal name="compute_max&#39;vc.21" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2584"/></proof>
</goal>
<goal name="compute_max&#39;vc.22" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="compute_max&#39;vc.23" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="2504"/></proof>
</goal>
<goal name="compute_max&#39;vc.24" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</transf>
</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