Skip to content
Snippets Groups Projects
Commit 6e6adc81 authored by Per Lindgren's avatar Per Lindgren
Browse files

polished imp_test

parent e6809fcc
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
imp_test/why3session.xml
+ 18
− 222
View file @ 6e6adc81
...@@ -2,236 +2,32 @@ ...@@ -2,236 +2,32 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../imp_test.mlw" proved="true">
<file name="../state.mlw" proved="true"> <theory name="Imp_test" proved="true">
<theory name="State" proved="true"> <goal name="ex1" proved="true">
<goal name="VC get" expl="VC for get" proved="true"> <proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
<goal name="VC set" expl="VC for set" proved="true"> <goal name="ex2" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="101"/></proof>
</goal> </goal>
<goal name="VC mixfix []" expl="VC for mixfix []" proved="true"> <goal name="ex3" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="97"/></proof>
</goal>
<goal name="VC mixfix [&lt;-]" expl="VC for mixfix [<-]" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC const" expl="VC for const" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="Reg" proved="true">
<goal name="VC read" expl="VC for read" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC write" expl="VC for write" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC const" expl="VC for const" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
</file>
<file name="../imp_test.mlw">
<theory name="Imp_test">
<goal name="ex1">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
<goal name="ex2">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="101"/></proof>
</goal>
<goal name="ex3">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="ex4" proved="true"> <goal name="ex4" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="97"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="97"/></proof>
</goal>
<goal name="ex5">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
</goal>
<goal name="ex6">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof>
</goal>
<goal name="ex7">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ex8">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof>
</goal>
</theory>
</file>
<file name="../imp_ex.mlw" proved="true">
<theory name="Imp_Ex" proved="true">
<goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="783"/></proof>
</goal> </goal>
<goal name="VC beval_ex" expl="VC for beval_ex" proved="true"> <goal name="ex5" proved="true">
<proof prover="0"><result status="valid" time="0.22" steps="667"/></proof> <proof prover="0"><result status="valid" time="0.04" steps="97"/></proof>
</goal> </goal>
<goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true"> <goal name="ex6" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="237"/></proof>
</goal>
</theory>
</file>
<file name="../imp_ex_assignment.mlw">
<theory name="Imp_ex">
<goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.68" steps="783"/></proof>
</goal>
<goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.20" steps="667"/></proof>
</goal>
<goal name="VC ceval_ex" expl="VC for ceval_ex">
<transf name="split_vc" >
<goal name="VC ceval_ex.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="74"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
</goal> </goal>
<goal name="VC ceval_ex.1" expl="postcondition"> <goal name="ex7" proved="true">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC ceval_ex.2" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC ceval_ex.3" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC ceval_ex.4" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
<file name="../imp.mlw" proved="true">
<theory name="Imp" proved="true">
<goal name="ceval_deterministic_aux" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.0" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="135"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="180"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.2.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal> </goal>
<goal name="ceval_deterministic_aux.2.1" proved="true"> <goal name="ex8" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="100"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.2" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.4" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.5" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.6" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.3" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.3.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.1" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.3" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.4" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.5" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.6" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.4" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.4.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.1" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.2" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.4" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.5" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.6" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.5" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="133"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.6.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.1" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.4" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.5" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.6" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="107"/></proof>
</goal>
<goal name="VC beval">
<proof prover="0"><result status="valid" time="0.02" steps="73"/></proof>
</goal>
<goal name="VC aeval">
<proof prover="0"><result status="valid" time="0.01" steps="73"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
imp_test/why3session.xml.bak deleted 100644 → 0
+ 0
− 238
View file @ e6809fcc
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../state.mlw" proved="true">
<theory name="State" proved="true">
<goal name="VC get" expl="VC for get" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC set" expl="VC for set" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC mixfix [&lt;-]" expl="VC for mixfix [<-]" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC const" expl="VC for const" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="Reg" proved="true">
<goal name="VC read" expl="VC for read" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC write" expl="VC for write" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC const" expl="VC for const" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
</file>
<file name="../imp_test.mlw">
<theory name="Imp_test">
<goal name="ex1" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
<goal name="ex2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="101"/></proof>
</goal>
<goal name="ex3" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="97"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="ex4">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
</goal>
<goal name="ex5">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
</goal>
<goal name="ex6">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof>
</goal>
<goal name="ex7">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ex8">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof>
</goal>
</theory>
</file>
<file name="../imp_ex_assignment.mlw">
<theory name="Imp_ex">
<goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.68" steps="783"/></proof>
</goal>
<goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.20" steps="667"/></proof>
</goal>
<goal name="VC ceval_ex" expl="VC for ceval_ex">
<transf name="split_vc" >
<goal name="VC ceval_ex.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
</goal>
<goal name="VC ceval_ex.1" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC ceval_ex.2" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC ceval_ex.3" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC ceval_ex.4" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
<file name="../imp_ex.mlw" proved="true">
<theory name="Imp_Ex" proved="true">
<goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="783"/></proof>
</goal>
<goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.22" steps="667"/></proof>
</goal>
<goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="237"/></proof>
</goal>
</theory>
</file>
<file name="../imp.mlw" proved="true">
<theory name="Imp" proved="true">
<goal name="ceval_deterministic_aux" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.0" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="135"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="180"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.2.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.1" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.2" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.4" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.5" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.6" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.3" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.3.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.1" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.3" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.4" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.5" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.6" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.4" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.4.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.1" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.2" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.4" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.5" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.6" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.5" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="133"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="ceval_deterministic_aux.6.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.1" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.4" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.5" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.6" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="107"/></proof>
</goal>
<goal name="VC beval">
<proof prover="0"><result status="valid" time="0.02" steps="73"/></proof>
</goal>
<goal name="VC aeval">
<proof prover="0"><result status="valid" time="0.01" steps="73"/></proof>
</goal>
</theory>
</file>
</why3session>
imp_test/why3shapes.gz
+ 0
− 0
View file @ 6e6adc81
No preview for this file type
imp_test/why3shapes.gz.bak deleted 100644 → 0
+ 0
− 0
View file @ e6809fcc
File deleted
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment