modules/array: added missing proofs

parent 72c977ea
......@@ -3,9 +3,11 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../../../modules/array.mlw" expanded="true">
<file name="../../../modules/array.mlw">
<theory name="Array" sum="324e125dff69cfce0eefc07a77b17b42">
<goal name="WP_parameter defensive_get" expl="VC for defensive_get">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
......@@ -20,15 +22,15 @@
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="IntArraySorted" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="IntArraySorted" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Sorted" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Sorted" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ArrayEq" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="ArrayEq" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ArrayExchange" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="ArrayExchange" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ArrayPermut" sum="c35e6a30805f654f329783c9ec01270c" expanded="true">
<theory name="ArrayPermut" sum="c35e6a30805f654f329783c9ec01270c">
<goal name="exchange_permut_sub">
<proof prover="2" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="3.65"/></proof>
</goal>
......@@ -45,13 +47,47 @@
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="ArraySum" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="ArraySum" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="NumOf" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="NumOf" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="NumOfEq" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="NumOfEq" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ToList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="ToList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ToSeq" sum="4d13eb3ec2ac0cea8847c8b058ea3d8b">
<goal name="WP_parameter to_seq_length" expl="VC for to_seq_length">
<transf name="split_goal_wp">
<goal name="WP_parameter to_seq_length.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter to_seq_length.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter to_seq_length.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter to_seq_length.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter to_seq_nth" expl="VC for to_seq_nth">
<transf name="split_goal_wp">
<goal name="WP_parameter to_seq_nth.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter to_seq_nth.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter to_seq_nth.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter to_seq_nth.4" expl="4. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -316,13 +316,19 @@ module ToSeq
forall a: array 'a, l u: int. 0 <= l < u <= length a ->
to_seq a l u = S.cons a[l] (to_seq a (l+1) u)
lemma to_seq_nth:
forall a: array 'a, l i u: int. 0 <= l <= i < u <= length a ->
S.get (to_seq a l u) (i - l) = a[i]
lemma to_seq_length:
forall a: array 'a, l u: int. 0 <= l <= u <= length a ->
S.length (to_seq a l u) = u - l
let rec lemma to_seq_length
(a: array 'a) (l u: int)
requires { 0 <= l <= u <= length a }
variant { u - l }
ensures { S.length (to_seq a l u) = u - l }
= if l < u then to_seq_length a (l+1) u
let rec lemma to_seq_nth
(a: array 'a) (l i u: int)
requires { 0 <= l <= i < u <= length a }
variant { i - l }
ensures { S.get (to_seq a l u) (i - l) = a[i] }
= if l < i then to_seq_nth a (l+1) i u
val to_seq (a: array 'a) (l u: int) : S.seq 'a
requires { 0 <= l && u <= length a }
......
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