Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit a1c9da89 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Prove remaining VC.

parent ec559214
......@@ -901,13 +901,13 @@
</file>
<file
name="../heap_implem.mlw"
verified="false"
verified="true"
expanded="true">
<theory
name="Implementation"
locfile="programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
loclnum="2" loccnumb="7" loccnume="21"
verified="false"
verified="true"
expanded="true">
<goal
name="Is_heap_min"
......@@ -1769,14 +1769,14 @@
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="0c1e79abf1fd054c99f43f632b0eea52"
proved="false"
proved="true"
expanded="true"
shape="iainfix &lt;V2ainfix -V1c1iainfix &gt;=ainfix +ainfix *c2V2c1ainfix -V1c1iainfix &lt;V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV5c0V6Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V5V6Iainfix =V6ainfix -V1c1Aainfix =V5V4FAainfix =aelementsV4c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aais_heap_arrayV4c0ainfix -V1c1Aais_heap_arrayV4c0ainfix -V1c1Iainfix &gt;V2c0Iainfix =V4amixfix [&lt;-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV7c0V8Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V7V8Iainfix =V8ainfix -V1c1Aainfix =V7V3Fiainfix &lt;ainfix +ainfix *c2V2c2ainfix -V1c1iainfix &gt;amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2iainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3V9iainfix &lt;V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV11c0V12Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V11V12Iainfix =V12ainfix -V1c1Aainfix =V11V10FAainfix =aelementsV10c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aais_heap_arrayV10c0ainfix -V1c1Aais_heap_arrayV10c0ainfix -V1c1Iainfix &gt;V2c0Iainfix =V10amixfix [&lt;-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV13c0V14Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V13V14Iainfix =V14ainfix -V1c1Aainfix =V13V3Fainfix &lt;ainfix -ainfix -V1c1V16ainfix -ainfix -V1c1V2Aainfix &lt;=c0ainfix -ainfix -V1c1V2Aainfix &lt;amixfix []V15aparentV16amixfix []V0ainfix -V1c1Iainfix &gt;V16c0Aainfix =aelementsV15c0ainfix -V1c1aaddamixfix []V15V16adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V15V0Iainfix =V16c0Aais_heap_arrayV15c0ainfix -V1c1Aainfix &lt;V16ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V16Iainfix =V16V9FIainfix =V15amixfix [&lt;-]V3V2amixfix []V3V9FIainfix =V9ainfix +ainfix *c2V2c2Fiainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1iainfix &lt;V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV18c0V19Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V18V19Iainfix =V19ainfix -V1c1Aainfix =V18V17FAainfix =aelementsV17c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aais_heap_arrayV17c0ainfix -V1c1Aais_heap_arrayV17c0ainfix -V1c1Iainfix &gt;V2c0Iainfix =V17amixfix [&lt;-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV20c0V21Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V20V21Iainfix =V21ainfix -V1c1Aainfix =V20V3Fainfix &lt;ainfix -ainfix -V1c1V23ainfix -ainfix -V1c1V2Aainfix &lt;=c0ainfix -ainfix -V1c1V2Aainfix &lt;amixfix []V22aparentV23amixfix []V0ainfix -V1c1Iainfix &gt;V23c0Aainfix =aelementsV22c0ainfix -V1c1aaddamixfix []V22V23adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V22V0Iainfix =V23c0Aais_heap_arrayV22c0ainfix -V1c1Aainfix &lt;V23ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V23Iainfix =V23ainfix +ainfix *c2V2c1FIainfix =V22amixfix [&lt;-]V3V2amixfix []V3ainfix +ainfix *c2V2c1Fiainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1iainfix &lt;V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV25c0V26Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V25V26Iainfix =V26ainfix -V1c1Aainfix =V25V24FAainfix =aelementsV24c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aais_heap_arrayV24c0ainfix -V1c1Aais_heap_arrayV24c0ainfix -V1c1Iainfix &gt;V2c0Iainfix =V24amixfix [&lt;-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV27c0V28Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V27V28Iainfix =V28ainfix -V1c1Aainfix =V27V3Fainfix &lt;ainfix -ainfix -V1c1V30ainfix -ainfix -V1c1V2Aainfix &lt;=c0ainfix -ainfix -V1c1V2Aainfix &lt;amixfix []V29aparentV30amixfix []V0ainfix -V1c1Iainfix &gt;V30c0Aainfix =aelementsV29c0ainfix -V1c1aaddamixfix []V29V30adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V29V0Iainfix =V30c0Aais_heap_arrayV29c0ainfix -V1c1Aainfix &lt;V30ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V30Iainfix =V30ainfix +ainfix *c2V2c1FIainfix =V29amixfix [&lt;-]V3V2amixfix []V3ainfix +ainfix *c2V2c1Fiainfix &lt;V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV32c0V33Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V32V33Iainfix =V33ainfix -V1c1Aainfix =V32V31FAainfix =aelementsV31c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aais_heap_arrayV31c0ainfix -V1c1Aais_heap_arrayV31c0ainfix -V1c1Iainfix &gt;V2c0Iainfix =V31amixfix [&lt;-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV34c0V35Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V34V35Iainfix =V35ainfix -V1c1Aainfix =V34V3FAainfix =ainfix -V1c1c0Iainfix &lt;amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix &gt;V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix &lt;V2ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V2FAainfix &lt;amixfix []V0aparentc0amixfix []V0ainfix -V1c1Iainfix &gt;c0c0Aainfix =aelementsV0c0ainfix -V1c1aaddamixfix []V0c0adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V0V0Iainfix =c0c0Aais_heap_arrayV0c0ainfix -V1c1Aainfix &lt;c0ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0c0Aainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Aainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter extractMin.1"
......@@ -1849,14 +1849,14 @@
loclnum="61" loccnumb="4" loccnume="14"
expl="loop invariant init"
sum="eeae44d8666068e174b01917ce1809c2"
proved="false"
proved="true"
expanded="true"
shape="ainfix &lt;amixfix []V0aparentc0amixfix []V0ainfix -V1c1Iainfix &gt;c0c0Aainfix =aelementsV0c0ainfix -V1c1aaddamixfix []V0c0adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V0V0Iainfix =c0c0Aais_heap_arrayV0c0ainfix -V1c1Aainfix &lt;c0ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0c0Iainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Iainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter extractMin.3.1"
......@@ -2004,11 +2004,43 @@
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="1e17d5359b618367513752d649acaffa"
proved="false"
proved="true"
expanded="false"
shape="ainfix =V0V0Iainfix =c0c0Iainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Iainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<proof
prover="11"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.3.5"
......
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