Commit 6589d1dc authored by Martin Clochard's avatar Martin Clochard

Prover example: fixed some proofs

parent b7f1a976
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<file name="../Firstorder_formula_list_spec.mlw" expanded="true">
<theory name="Spec" sum="95246be42438773cb85bab6d78509d88" expanded="true">
<theory name="Spec" sum="95246be42438773cb85bab6d78509d88">
<goal name="WP_parameter size_positive_lemma_fo_formula_list" expl="VC for size_positive_lemma_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.10" steps="63"/></proof>
</goal>
......@@ -19,7 +19,7 @@
<proof prover="2" timelimit="1"><result status="valid" time="0.22" steps="154"/></proof>
</goal>
<goal name="WP_parameter subst_then_rename_composition_lemma_fo_formula_list" expl="VC for subst_then_rename_composition_lemma_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="191"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.12" steps="191"/></proof>
</goal>
<goal name="WP_parameter subst_composition_lemma_fo_formula_list" expl="VC for subst_composition_lemma_fo_formula_list">
<transf name="split_goal_wp">
......@@ -65,16 +65,16 @@
<proof prover="2"><result status="valid" time="0.09" steps="57"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_constructive_inversion_fo_term_fo_formula_list" expl="VC for subst_free_var_constructive_inversion_fo_term_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.28" steps="386"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.14" steps="386"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_fo_term_fo_formula_list" expl="VC for subst_free_var_inversion_fo_term_fo_formula_list">
<proof prover="2" timelimit="1"><result status="valid" time="0.07" steps="9"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_symbol_symbol_fo_formula_list" expl="VC for subst_free_var_propagation_symbol_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="0.60" steps="1036"/></proof>
<proof prover="2"><result status="valid" time="0.51" steps="1036"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_symbol_fo_formula_list" expl="VC for subst_free_var_propagation_fo_term_symbol_fo_formula_list">
<proof prover="2"><result status="valid" time="1.11" steps="652"/></proof>
<proof prover="2"><result status="valid" time="0.76" steps="652"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_propagation_fo_term_fo_term_fo_formula_list" expl="VC for subst_free_var_propagation_fo_term_fo_term_fo_formula_list">
<transf name="split_goal_wp">
......@@ -110,7 +110,7 @@
<proof prover="2"><result status="valid" time="0.10" steps="7"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.3" expl="3. precondition">
<proof prover="2"><result status="valid" time="0.75" steps="132"/></proof>
<proof prover="2"><result status="valid" time="0.46" steps="132"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_fo_formula_list.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.18" steps="154"/></proof>
......@@ -150,10 +150,10 @@
<proof prover="2"><result status="valid" time="0.10" steps="45"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.4" expl="4. postcondition">
<proof prover="3"><result status="valid" time="1.57"/></proof>
<proof prover="1"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_fo_formula_list.5" expl="5. postcondition">
<proof prover="3"><result status="valid" time="1.59"/></proof>
<proof prover="1"><result status="valid" time="0.74"/></proof>
</goal>
</transf>
</goal>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<file name="../Firstorder_tableau_spec.mlw" expanded="true">
<theory name="Spec" sum="04ae47ccff643d8e6498166eda7f9b58" expanded="true">
<theory name="Spec" sum="04ae47ccff643d8e6498166eda7f9b58">
<goal name="WP_parameter size_positive_lemma_tableau" expl="VC for size_positive_lemma_tableau">
<proof prover="2"><result status="valid" time="0.16" steps="70"/></proof>
</goal>
......@@ -16,10 +16,10 @@
<proof prover="2"><result status="valid" time="0.10" steps="48"/></proof>
</goal>
<goal name="WP_parameter rename_then_subst_composition_lemma_tableau" expl="VC for rename_then_subst_composition_lemma_tableau">
<proof prover="2"><result status="valid" time="1.38" steps="116"/></proof>
<proof prover="2"><result status="valid" time="0.94" steps="116"/></proof>
</goal>
<goal name="WP_parameter subst_then_rename_composition_lemma_tableau" expl="VC for subst_then_rename_composition_lemma_tableau">
<proof prover="2"><result status="valid" time="0.40" steps="239"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="239"/></proof>
</goal>
<goal name="WP_parameter subst_composition_lemma_tableau" expl="VC for subst_composition_lemma_tableau">
<transf name="split_goal_wp">
......@@ -59,13 +59,13 @@
<proof prover="2"><result status="valid" time="0.22" steps="221"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_constructive_inversion_symbol_tableau" expl="VC for subst_free_var_constructive_inversion_symbol_tableau">
<proof prover="2"><result status="valid" time="0.61" steps="840"/></proof>
<proof prover="2"><result status="valid" time="0.29" steps="840"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_symbol_tableau" expl="VC for subst_free_var_inversion_symbol_tableau">
<proof prover="2"><result status="valid" time="0.12" steps="54"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_constructive_inversion_fo_term_tableau" expl="VC for subst_free_var_constructive_inversion_fo_term_tableau">
<proof prover="2"><result status="valid" time="0.42" steps="448"/></proof>
<proof prover="2"><result status="valid" time="0.20" steps="448"/></proof>
</goal>
<goal name="WP_parameter subst_free_var_inversion_fo_term_tableau" expl="VC for subst_free_var_inversion_fo_term_tableau">
<proof prover="2"><result status="valid" time="0.08" steps="9"/></proof>
......@@ -137,13 +137,13 @@
</transf>
</goal>
<goal name="WP_parameter free_var_equivalence_of_subst_tableau" expl="VC for free_var_equivalence_of_subst_tableau">
<proof prover="2"><result status="valid" time="0.35" steps="563"/></proof>
<proof prover="2"><result status="valid" time="0.17" steps="563"/></proof>
</goal>
<goal name="WP_parameter free_var_equivalence_of_rename_tableau" expl="VC for free_var_equivalence_of_rename_tableau">
<proof prover="2"><result status="valid" time="0.17" steps="251"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_subst_tableau" expl="VC for free_var_derive_equivalence_of_subst_tableau">
<proof prover="2"><result status="valid" time="0.64" steps="935"/></proof>
<proof prover="2"><result status="valid" time="0.39" steps="935"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_tableau" expl="VC for free_var_derive_equivalence_of_rename_tableau">
<transf name="split_goal_wp">
......@@ -157,10 +157,10 @@
<proof prover="2"><result status="valid" time="0.12" steps="45"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_tableau.4" expl="4. postcondition">
<proof prover="3"><result status="valid" time="1.36"/></proof>
<proof prover="0"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="WP_parameter free_var_derive_equivalence_of_rename_tableau.5" expl="5. postcondition">
<proof prover="3"><result status="valid" time="1.52"/></proof>
<proof prover="0"><result status="valid" time="0.87"/></proof>
</goal>
</transf>
</goal>
......
......@@ -1283,9 +1283,7 @@ module Impl
requires { is_nnf_list l.model_fo_formula_list_field }
requires { is_simpl phi0.model_fo_formula_field }
requires { is_nnf phi0.model_fo_formula_field }
(* this variant does not work: we now nothing about the size of
the list returned by destruct_fo_formula_list :-( *)
variant { nlsize_fo_formula_list l.nlrepr_fo_formula_list_field }
variant { size_fo_formula_list l.model_fo_formula_list_field }
ensures { nlimpl_fo_formula_ok result.form }
ensures { is_simpl result.form.model_fo_formula_field }
ensures { is_nnf result.form.model_fo_formula_field }
......@@ -1330,9 +1328,7 @@ module Impl
requires { is_simpl_list l.model_fo_formula_list_field }
requires { is_nnf_list l.model_fo_formula_list_field }
requires { no_existential_list l.model_fo_formula_list_field }
(* this variant does not work: we now nothing about the size of
the formula returned by destruct_fo_formula :-( *)
variant { nlsize_fo_formula phi.nlrepr_fo_formula_field }
variant { size_fo_formula phi.model_fo_formula_field }
ensures { forall m:model int 'st,rho:func int 'st.
formula_list_conj_semantic result.forms.model_fo_formula_list_field m rho
<-> (formula_semantic phi.model_fo_formula_field m rho /\
......
......@@ -3,16 +3,16 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../Functions.mlw" expanded="true">
<theory name="Func" sum="91c29f6d1ccbb18c7b87b2cd3454d039" expanded="true">
<file name="../Functions.mlw">
<theory name="Func" sum="91c29f6d1ccbb18c7b87b2cd3454d039">
<goal name="update_eq">
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="update_neq">
<proof prover="1"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter compose_associative" expl="VC for compose_associative">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter identity_neutral" expl="VC for identity_neutral">
<proof prover="1"><result status="valid" time="0.02" steps="38"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
<file name="../ISet.mlw" expanded="true">
<file name="../ISet.mlw">
<theory name="Types" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Logic" sum="1832f7e6a08d37d0e5b072192d8369d1">
......@@ -17,7 +17,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter iset_ok_char.3" expl="3. assertion">
<proof prover="3"><result status="valid" time="0.13"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter iset_ok_char.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.11" steps="281"/></proof>
......@@ -130,7 +130,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter merge.11" expl="11. postcondition">
<proof prover="2"><result status="valid" time="0.68" steps="891"/></proof>
<proof prover="2"><result status="valid" time="0.42" steps="891"/></proof>
</goal>
<goal name="WP_parameter merge.12" expl="12. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -148,7 +148,7 @@
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter merge.17" expl="17. postcondition">
<proof prover="2"><result status="valid" time="0.69" steps="739"/></proof>
<proof prover="2"><result status="valid" time="0.37" steps="739"/></proof>
</goal>
<goal name="WP_parameter merge.18" expl="18. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="29"/></proof>
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../Nat.mlw">
<file name="../Nat.mlw" expanded="true">
<theory name="Nat" sum="93803c23acf28091314de05391da648a">
<goal name="WP_parameter nat_to_int_nonnegative" expl="VC for nat_to_int_nonnegative">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
......
......@@ -5,17 +5,17 @@
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../Predicates.mlw" expanded="true">
<theory name="Pred" sum="ac803a6d54d377b1900e06a191a70737" expanded="true">
<goal name="pupdate_eq">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
<goal name="pupdate_eq" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="pupdate_neq">
<goal name="pupdate_neq" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter pcompose_associative" expl="VC for pcompose_associative">
<goal name="WP_parameter pcompose_associative" expl="VC for pcompose_associative" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter identity_neutral" expl="VC for identity_neutral">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
<goal name="WP_parameter identity_neutral" expl="VC for identity_neutral" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></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