Skip to content
GitLab
Commit 3ec2ee15 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update missing proofs

parent 51b157da
Hide whitespace changes
Inline Side-by-side
examples/programs/vacid_0_binary_heaps/proofs/why3session.xml
View file @ 3ec2ee15
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="proofs/why3session.xml">
name="examples/programs/vacid_0_binary_heaps/proofs/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......@@ -1644,11 +1644,11 @@
<file
name="../heap_implem.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="WP Implementation"
verified="true"
expanded="false">
expanded="true">
<goal
name="Is_heap_min"
sum="6cf89b9ccf7e6bd6c1337ab8a005af90"
......@@ -2193,12 +2193,12 @@
expl="parameter extractMin"
sum="5af2eeafdebbb8bb11b9a9b2a0bcd772"
proved="true"
expanded="false"
expanded="true"
shape="iainfix <V2ainfix -V1c1iainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1iainfix <V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV5c0V6Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V5V6Iainfix =aTuple2V5V6aTuple2V4ainfix -V1c1FAainfix =aelementsV4c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aais_heap_arrayV4c0ainfix -V1c1Aais_heap_arrayV4c0ainfix -V1c1Iainfix >V2c0Iainfix =V4amixfix [<-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV7c0V8Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V7V8Iainfix =aTuple2V7V8aTuple2V3ainfix -V1c1Fiainfix <ainfix +ainfix *c2V2c2ainfix -V1c1iainfix >amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2iainfix <=amixfix []V0ainfix -V1c1amixfix []V3V9iainfix <V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV11c0V12Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V11V12Iainfix =aTuple2V11V12aTuple2V10ainfix -V1c1FAainfix =aelementsV10c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aais_heap_arrayV10c0ainfix -V1c1Aais_heap_arrayV10c0ainfix -V1c1Iainfix >V2c0Iainfix =V10amixfix [<-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV13c0V14Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V13V14Iainfix =aTuple2V13V14aTuple2V3ainfix -V1c1Fainfix <ainfix -ainfix -V1c1V16ainfix -ainfix -V1c1V2Aainfix <=c0ainfix -ainfix -V1c1V2Aainfix <amixfix []V15aparentV16amixfix []V0ainfix -V1c1Iainfix >V16c0Aainfix =aelementsV15c0ainfix -V1c1aaddamixfix []V15V16adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V15V0Iainfix =V16c0Aais_heap_arrayV15c0ainfix -V1c1Aainfix <V16ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V16Iainfix =V16V9FIainfix =V15amixfix [<-]V3V2amixfix []V3V9FIainfix =V9ainfix +ainfix *c2V2c2Fiainfix <=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1iainfix <V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV18c0V19Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V18V19Iainfix =aTuple2V18V19aTuple2V17ainfix -V1c1FAainfix =aelementsV17c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aais_heap_arrayV17c0ainfix -V1c1Aais_heap_arrayV17c0ainfix -V1c1Iainfix >V2c0Iainfix =V17amixfix [<-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV20c0V21Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V20V21Iainfix =aTuple2V20V21aTuple2V3ainfix -V1c1Fainfix <ainfix -ainfix -V1c1V23ainfix -ainfix -V1c1V2Aainfix <=c0ainfix -ainfix -V1c1V2Aainfix <amixfix []V22aparentV23amixfix []V0ainfix -V1c1Iainfix >V23c0Aainfix =aelementsV22c0ainfix -V1c1aaddamixfix []V22V23adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V22V0Iainfix =V23c0Aais_heap_arrayV22c0ainfix -V1c1Aainfix <V23ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V23Iainfix =V23ainfix +ainfix *c2V2c1FIainfix =V22amixfix [<-]V3V2amixfix []V3ainfix +ainfix *c2V2c1Fiainfix <=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1iainfix <V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV25c0V26Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V25V26Iainfix =aTuple2V25V26aTuple2V24ainfix -V1c1FAainfix =aelementsV24c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aais_heap_arrayV24c0ainfix -V1c1Aais_heap_arrayV24c0ainfix -V1c1Iainfix >V2c0Iainfix =V24amixfix [<-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV27c0V28Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V27V28Iainfix =aTuple2V27V28aTuple2V3ainfix -V1c1Fainfix <ainfix -ainfix -V1c1V30ainfix -ainfix -V1c1V2Aainfix <=c0ainfix -ainfix -V1c1V2Aainfix <amixfix []V29aparentV30amixfix []V0ainfix -V1c1Iainfix >V30c0Aainfix =aelementsV29c0ainfix -V1c1aaddamixfix []V29V30adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V29V0Iainfix =V30c0Aais_heap_arrayV29c0ainfix -V1c1Aainfix <V30ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V30Iainfix =V30ainfix +ainfix *c2V2c1FIainfix =V29amixfix [<-]V3V2amixfix []V3ainfix +ainfix *c2V2c1Fiainfix <V2ainfix -V1c1ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV32c0V33Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V32V33Iainfix =aTuple2V32V33aTuple2V31ainfix -V1c1FAainfix =aelementsV31c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aais_heap_arrayV31c0ainfix -V1c1Aais_heap_arrayV31c0ainfix -V1c1Iainfix >V2c0Iainfix =V31amixfix [<-]V3V2amixfix []V0ainfix -V1c1Fainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV34c0V35Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V34V35Iainfix =aTuple2V34V35aTuple2V3ainfix -V1c1FAainfix =ainfix -V1c1c0Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFAainfix <amixfix []V0aparentc0amixfix []V0ainfix -V1c1Iainfix >c0c0Aainfix =aelementsV0c0ainfix -V1c1aaddamixfix []V0c0adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V0V0Iainfix =c0c0Aais_heap_arrayV0c0ainfix -V1c1Aainfix <c0ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0c0Aainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Aainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<transf
name="split_goal"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter extractMin.1"
expl="assertion"
......@@ -3902,21 +3902,21 @@
expl="assertion"
sum="a0fe798aa32803eb046d4ab8d28b0f33"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aelementsV4c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Iais_heap_arrayV4c0ainfix -V1c1Iais_heap_arrayV4c0ainfix -V1c1Iainfix >V2c0Iainfix =V4amixfix [<-]V3V2amixfix []V0ainfix -V1c1FIainfix <V2ainfix -V1c1Iainfix =ainfix -V1c1c0Iainfix <V2ainfix -V1c1NIainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<proof
prover="cvc3"
timelimit="3"
edited=""
obsolete="false"><undone/>
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="30"
edited=""
obsolete="false"><undone/>
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="z3"
......@@ -3938,7 +3938,7 @@
expl="normal postcondition"
sum="8b174250fa069ad4395287ee3f33bf5c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV5c0V6Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V5V6Iainfix =aTuple2V5V6aTuple2V4ainfix -V1c1FIainfix =aelementsV4c0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Iais_heap_arrayV4c0ainfix -V1c1Iais_heap_arrayV4c0ainfix -V1c1Iainfix >V2c0Iainfix =V4amixfix [<-]V3V2amixfix []V0ainfix -V1c1FIainfix <V2ainfix -V1c1Iainfix =ainfix -V1c1c0Iainfix <V2ainfix -V1c1NIainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<proof
prover="cvc3"
......@@ -3974,7 +3974,7 @@
expl="normal postcondition"
sum="20d782c1c65f0db15eb800ff2b8a2989"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aelementsV0c0V1aaddamixfix []V0c0aelementsV4c0V5Aainfix =amixfix []V0c0amin_bagaelementsV0c0V1Aais_heapaTuple2V4V5Iainfix =aTuple2V4V5aTuple2V3ainfix -V1c1FIainfix <V2ainfix -V1c1NIainfix =ainfix -V1c1c0Iainfix <V2ainfix -V1c1NIainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<proof
prover="cvc3"
......
Supports Markdown
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