Commit 0ac3a7ec authored by MARCHE Claude's avatar MARCHE Claude

a minor fix and a real example

parent 6f77d846
This diff is collapsed.
module MaxArray
use int.Int
use array.Array
let cfg compute_max (a:array int) : (max: int, ind:int)
requires { a.length > 0 }
ensures { forall i. 0 <= i < a.length -> a[ind] >= a[i] }
=
(* simulation of the C code: (from ACSL Manual, section 2.4.2 Loop invariants)
i = 0;
goto L;
do {
if (t[i] > m) { L: m = t[i]; }
/*@ invariant
@ 0 <= i < n && m == \max(0,i,\lambda integer k; t[k]);
@*/
i++;
}
while (i < n);
return m;
*)
var (i m:int);
var (ind:int); (* should be ghost *)
{
i <- 0;
goto L
}
L {
m <- a[i];
ind <- i;
goto L1
}
L1 {
invariant I { 0 <= i < a.length /\
0 <= ind < a.length /\
m = a[ind] /\
forall j. 0 <= j <= i -> a[ind] >= a[j] };
(* (yes, j <= i, not j < i !) *)
i <- i+1;
switch (i < a.length) with
| True -> goto L2
| False -> (m,ind)
end
}
L2 {
switch (a[i] > m) with
| True -> goto L
| False -> 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="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="max_array.mlcfg"/>
<theory name="MaxArray" proved="true">
<goal name="compute_max&#39;vc" expl="VC for compute_max" proved="true">
<transf name="split_vc" proved="true" >
<goal name="compute_max&#39;vc.0" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="2638"/></proof>
</goal>
<goal name="compute_max&#39;vc.1" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3086"/></proof>
</goal>
<goal name="compute_max&#39;vc.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3038"/></proof>
</goal>
<goal name="compute_max&#39;vc.3" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3001"/></proof>
</goal>
<goal name="compute_max&#39;vc.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3044"/></proof>
</goal>
<goal name="compute_max&#39;vc.5" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3758"/></proof>
</goal>
<goal name="compute_max&#39;vc.6" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="3643"/></proof>
</goal>
<goal name="compute_max&#39;vc.7" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3654"/></proof>
</goal>
<goal name="compute_max&#39;vc.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3596"/></proof>
</goal>
<goal name="compute_max&#39;vc.9" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3237"/></proof>
</goal>
<goal name="compute_max&#39;vc.10" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2965"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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