Commit c1d0e321 authored by MARCHE Claude's avatar MARCHE Claude

update proofs of examples/stdlib

parent c527862b
......@@ -91,7 +91,7 @@ intros a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7.
destruct h1 as (h11,h12).
destruct h12 as (ha,(hb,(hc,(hd,he)))).
red. repeat split.
(* eq_sub *)
(* eq_sub *)
red. intros. apply he; omega.
assumption. assumption. omega. omega. assumption.
(* permut *)
......@@ -205,4 +205,3 @@ omega.
(* eq_sub *)
red. intros. apply he; omega.
Qed.
......@@ -5,27 +5,28 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" 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="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.6" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../../../modules/array.mlw" expanded="true">
<theory name="Array" sum="285c467dea3cde7aa3a3c699222d37ee">
<goal name="WP_parameter defensive_get" expl="VC for defensive_get">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<theory name="Array" sum="970b7405c759ecbe0c07f7a2b552e809">
<goal name="VC defensive_get" expl="VC for defensive_get">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter defensive_set" expl="VC for defensive_set">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<goal name="VC defensive_set" expl="VC for defensive_set">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fill" expl="VC for fill">
<proof prover="0"><result status="valid" time="0.02" steps="58"/></proof>
<goal name="VC fill" expl="VC for fill">
<proof prover="0"><result status="valid" time="0.02" steps="149"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter self_blit" expl="VC for self_blit">
<proof prover="2"><result status="valid" time="0.10" steps="148"/></proof>
<goal name="VC self_blit" expl="VC for self_blit">
<proof prover="2"><result status="valid" time="0.32" steps="605"/></proof>
</goal>
</theory>
<theory name="Init" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="IntArraySorted" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Sorted" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -34,20 +35,20 @@
</theory>
<theory name="ArrayExchange" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ArrayPermut" sum="c35e6a30805f654f329783c9ec01270c">
<theory name="ArrayPermut" sum="fa43aabf25fea9d71d1310e660ffa972">
<goal name="exchange_permut_sub">
<proof prover="5" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="1.57"/></proof>
</goal>
<goal name="permut_sub_weakening">
<proof prover="5" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="0.51"/></proof>
<proof prover="5" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="exchange_permut_all">
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="ArraySwap" sum="fd8901e039caebc94247a7f0ccc00e16">
<goal name="WP_parameter swap" expl="VC for swap">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
<theory name="ArraySwap" sum="7f838d1eeb430063a79b41c547f5a161">
<goal name="VC swap" expl="VC for swap">
<proof prover="0"><result status="valid" time="0.00" steps="20"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
......@@ -57,41 +58,41 @@
</theory>
<theory name="NumOfEq" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ToList" sum="b7bcfe4954496ee8ce9bf8d36ab68113">
<goal name="WP_parameter to_list_append" expl="VC for to_list_append">
<proof prover="2"><result status="valid" time="0.01" steps="34"/></proof>
<theory name="ToList" sum="1cfde67ed2807856253ce564c8a87788">
<goal name="VC to_list" expl="VC for to_list">
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC to_list_append" expl="VC for to_list_append">
<proof prover="2"><result status="valid" time="0.03" steps="118"/></proof>
</goal>
</theory>
<theory name="ToSeq" sum="972d3973679c1b19bf79339fb847c382">
<goal name="WP_parameter to_seq_length" expl="VC for to_seq_length">
<theory name="ToSeq" sum="92110e2d9bcac82fcbe10442f737b359">
<goal name="VC to_seq" expl="VC for to_seq">
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC 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 name="VC to_seq_length.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></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 name="VC to_seq_length.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></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 name="VC to_seq_length.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter to_seq_nth" expl="VC for to_seq_nth">
<goal name="VC 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 name="VC to_seq_nth.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></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 name="VC to_seq_nth.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter to_seq_nth.4" expl="4. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<goal name="VC to_seq_nth.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -322,7 +322,7 @@ module ToList
use import list.Append
let rec lemma to_list_append (a: array 'a) (l m u: int)
requires { l <= m <= u }
requires { 0 <= l <= m <= u <= a.length }
variant { m - l }
ensures { to_list a l m ++ to_list a m u = to_list a l u }
= if l < m then to_list_append a (l+1) m u
......
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