Commit 7f18b955 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

removed superfluous split + run every provers

parent 1fb3abff
......@@ -6,7 +6,7 @@
Author: Jean-Christophe Filliâtre *)
(*
Iterative deletion in a binary search tree - 90 minutest
Iterative deletion in a binary search tree - 90 minutes
VERIFICATION TASK
......@@ -141,9 +141,9 @@ module Treedel
let ghost ppr = ref (right it) in
let ghost subtree = ref (left it) in
while !tt <> null do
invariant { !pp <> null /\ !mem[!pp].left = !p /\
!p <> null /\ !mem[!p].left = !tt /\
let pt = Node !subtree !pp !ppr in
invariant { !pp <> null /\ !mem[!pp].left = !p }
invariant { !p <> null /\ !mem[!p].left = !tt }
invariant { let pt = Node !subtree !pp !ppr in
tree !mem !pp pt /\ zip pt !zipper = it }
assert { tree !mem !p !subtree };
ghost zipper := Left !zipper !pp !ppr;
......
......@@ -4,19 +4,43 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.93.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.94"/>
<prover
id="2"
name="Alt-Ergo"
version="0.95"/>
<prover
id="3"
name="CVC3"
version="2.2"/>
<prover
id="4"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
id="5"
name="CVC4"
version="1.0"/>
<prover
id="6"
name="Coq"
version="8.3pl4"/>
<prover
id="3"
id="7"
name="Z3"
version="2.19"/>
<prover
id="8"
name="Z3"
version="3.2"/>
<prover
id="9"
name="Z3"
version="4.2"/>
<file
name="../verifythis_fm2012_treedel.mlw"
verified="true"
......@@ -40,12 +64,76 @@
name="expl:VC for get_left"/>
<proof
prover="0"
timelimit="10"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter get_right"
......@@ -60,7 +148,71 @@
name="expl:VC for get_right"/>
<proof
prover="0"
timelimit="10"
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.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -80,7 +232,71 @@
name="expl:VC for get_data"/>
<proof
prover="0"
timelimit="10"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -93,7 +309,7 @@
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="71" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
expanded="false">
<goal
name="inorder_zip"
locfile="../verifythis_fm2012_treedel.mlw"
......@@ -130,12 +346,76 @@
shape="CV0aTopainfix =ainorderazipaNodeV2V1V3V0ainfix ++ainorderV2aConsV1ainorderazipV3V0FaLeftVVVtF">
<proof
prover="0"
timelimit="10"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="inorder_zip.1.2"
......@@ -148,43 +428,171 @@
shape="CV0aToptaLeftVVVainfix =ainorderazipaNodeV5V4V6V0ainfix ++ainorderV5aConsV4ainorderazipV6V0FIainfix =ainorderazipaNodeV8V7V9V1ainfix ++ainorderV8aConsV7ainorderazipV9V1FF">
<proof
prover="0"
timelimit="10"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.63"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.34"/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name="WP_parameter left"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="102" loccnumb="12" loccnume="16"
expl="VC for left"
sum="c270c450ae0472d0dac3e2278f02ab88"
proved="true"
expanded="false"
shape="CV0aEmptyfaNodeVwwCV0aEmptyfaNodeVwwainfix =V1V2Iainfix =V0aEmptyNF">
<label
name="expl:VC for left"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter right"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="107" loccnumb="12" loccnume="17"
expl="VC for right"
sum="aad404ea5b9e844f3226612924a1780e"
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.20"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.18"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.16"/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name="WP_parameter left"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="102" loccnumb="12" loccnume="16"
expl="VC for left"
sum="c270c450ae0472d0dac3e2278f02ab88"
proved="true"
expanded="false"
shape="CV0aEmptyfaNodeVwwCV0aEmptyfaNodeVwwainfix =V1V2Iainfix =V0aEmptyNF">
<label
name="expl:VC for left"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.15"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter right"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="107" loccnumb="12" loccnume="17"
expl="VC for right"
sum="aad404ea5b9e844f3226612924a1780e"
proved="true"
expanded="false"
shape="CV0aEmptyfaNodewwVCV0aEmptyfaNodewwVainfix =V1V2Iainfix =V0aEmptyNF">
......@@ -192,12 +600,76 @@
name="expl:VC for right"/>
<proof
prover="0"
timelimit="10"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>