Skip to content

GitLab

why3
why3
Commit 432af472 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

fixed more sessions

parent bdc24b61
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 353 additions and 537 deletions
examples/insertion_sort_naive.mlw
View file @ 432af472
......@@ -31,6 +31,7 @@ module InsertionSortNaive
invariant { sorted_sub a !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
a[k1] <= a[k2] }
variant { !j }
'L:
let b = !j - 1 in
let t = a[!j] in
......@@ -83,6 +84,7 @@ module InsertionSortNaiveGen
invariant { sorted_sub a !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le a[k1] a[k2] }
variant { !j }
'L:
let b = !j - 1 in
let t = a[!j] in
......@@ -142,6 +144,7 @@ module InsertionSortParam
invariant { sorted_sub p a.elts !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le p a[k1] a[k2] }
variant { !j }
'L:
let b = !j - 1 in
let t = a[!j] in
......@@ -201,6 +204,7 @@ module InsertionSortParamBad
invariant { sorted_sub p a !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le p a[k1] a[k2] }
variant { !j }
'L:
let b = !j - 1 in
let t = a[!j] in
......
examples/list_rev.mlw
View file @ 432af472
......@@ -114,6 +114,7 @@ module M
let list_rev (p : ref pointer)
requires { is_list !next !p }
diverges
ensures { is_list !next !result }
= let q = ref null in
while !p <> null do
......@@ -155,6 +156,7 @@ module M
let list_rev_behv (p : ref pointer)
requires { is_list !next !p }
diverges
ensures { is_list !next !result }
ensures { reverse (model (old !next) (old !p)) = model !next !result }
= let old_next = !next in
......@@ -281,6 +283,7 @@ module M2
let list_rev (p : ref pointer) =
requires { is_list !next !p }
diverges
ensures { is_list !next !result }
let q = ref null in
while !p <> null do
......@@ -335,6 +338,7 @@ module M2
invariant { sep_list_list !next !p !q }
invariant { reverse (model (at !next 'Init) (old_p)) =
reverse (model !next !p) ++ model !next !q }
variant { model !next !p }
let tmp = !next[!p] in
next := !next[!p <- !q];
(* assert { (reverse (Cons p (model !next tmp))) ++ (model !next q) = *)
......
examples/list_rev/why3session.xml
View file @ 432af472
......@@ -8,29 +8,25 @@
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
id="2"
name="CVC4"
version="1.2"/>
<prover
id="4"
id="3"
name="Coq"
version="8.4pl2"/>
<prover
id="5"
id="4"
name="Z3"
version="2.19"/>
<prover
id="6"
id="5"
name="Z3"
version="3.2"/>
<prover
id="7"
id="6"
name="Z3"
version="4.3.1"/>
<file
......@@ -49,32 +45,8 @@
loclnum="109" loccnumb="8" loccnume="20"
sum="8e7154c52c8377b7929688d83806151f"
proved="false"
expanded="false"
expanded="true"
shape="asep_node_listV0V1amixfix []V0V1Iais_listV0V1INainfix =V1anullF">
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.95"/>
</proof>
<proof
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.03"/>
</proof>
</goal>
<goal
name="consistent"
......@@ -82,56 +54,8 @@
loclnum="112" loccnumb="7" loccnume="17"
sum="32c32aa03da7f78c75dd6174e4d07021"
proved="false"
expanded="false"
expanded="true"
shape="fIais_listV0V2Iais_listV0V1F">
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.98"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.96"/>
</proof>
<proof
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.03"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter list_rev"
......@@ -145,7 +69,7 @@
<label
name="expl:VC for list_rev"/>
<proof
prover="2"
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -153,7 +77,7 @@
<result status="valid" time="0.29"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -161,7 +85,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -172,7 +96,7 @@
<goal
name="reverse_append"
locfile="../list_rev.mlw"
loclnum="145" loccnumb="8" loccnume="22"
loclnum="146" loccnumb="8" loccnume="22"
sum="f4a7d3d7295173ddd36ca208e53dcb35"
proved="true"
expanded="false"
......@@ -189,7 +113,7 @@
<goal
name="WP_parameter list_rev_behv"
locfile="../list_rev.mlw"
loclnum="156" loccnumb="6" loccnume="19"
loclnum="157" loccnumb="6" loccnume="19"
expl="VC for list_rev_behv"
sum="3bb826699001bba00adf7be9d76bf97f"
proved="true"
......@@ -198,15 +122,7 @@
<label
name="expl:VC for list_rev_behv"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.96"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -214,15 +130,7 @@
<result status="valid" time="5.59"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -230,33 +138,25 @@
<result status="valid" time="0.05"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.38"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.99"/>
</proof>
</goal>
</theory>
<theory
name="M2"
locfile="../list_rev.mlw"
loclnum="181" loccnumb="7" loccnume="9"
loclnum="182" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="is_list_disjoint_case"
locfile="../list_rev.mlw"
loclnum="206" loccnumb="7" loccnume="28"
loclnum="207" loccnumb="7" loccnume="28"
sum="3a84d3af75de509eddb28b7cacc40cd8"
proved="true"
expanded="false"
......@@ -273,13 +173,13 @@
<goal
name="frame_list"
locfile="../list_rev.mlw"
loclnum="252" loccnumb="8" loccnume="18"
loclnum="253" loccnumb="8" loccnume="18"
sum="d69a8f4e8239e572061ea96dbcc2bf62"
proved="true"
expanded="false"
shape="ais_listamixfix [&lt;-]V0V2V3V1Iais_listV0V1INain_ftV2alist_ftV0V1Fais_listamixfix [&lt;-]V0V2V3V1">
<proof
prover="4"
prover="3"
timelimit="10"
memlimit="0"
edited="list_rev_M2_frame_list_1.v"
......@@ -291,13 +191,13 @@
<goal
name="frame_list_ft"
locfile="../list_rev.mlw"
loclnum="263" loccnumb="8" loccnume="21"
loclnum="264" loccnumb="8" loccnume="21"
sum="aba0a6d8fcfe7b9215562390f0b83c2c"
proved="true"
expanded="false"
shape="ainfix =alist_ftV0V1alist_ftamixfix [&lt;-]V0V2V3V1Iais_listV0V1INain_ftV2alist_ftV0V1F">
<proof
prover="4"
prover="3"
timelimit="10"
memlimit="0"
edited="list_rev_M2_frame_list_ft_1.v"
......@@ -309,129 +209,25 @@
<goal
name="acyclic_list"
locfile="../list_rev.mlw"
loclnum="277" loccnumb="8" loccnume="20"
loclnum="278" loccnumb="8" loccnume="20"
sum="898fe73039b5442e8ca471097083180f"
proved="false"
expanded="false"
expanded="true"
shape="asep_node_listV0V1amixfix []V0V1Iais_listV0V1INainfix =V1anullF">
<proof
prover="0"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.19"/>
</proof>
<proof
prover="1"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.94"/>
</proof>
<proof
prover="2"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="59.65"/>
</proof>
<proof
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="consistent"
locfile="../list_rev.mlw"
loclnum="280" loccnumb="7" loccnume="17"
loclnum="281" loccnumb="7" loccnume="17"
sum="376a8e2fa6534a1b8ff7b480918e05c4"
proved="false"
expanded="false"
expanded="true"
shape="fIais_listV0V2Iais_listV0V1F">
<proof
prover="0"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.09"/>
</proof>
<proof
prover="2"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="59.62"/>
</proof>
<proof
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter list_rev"
locfile="../list_rev.mlw"
loclnum="283" loccnumb="6" loccnume="14"
loclnum="284" loccnumb="6" loccnume="14"
expl="VC for list_rev"
sum="1407f9a2d3dba02254b30cbe1de20993"
proved="true"
......@@ -440,7 +236,7 @@
<label
name="expl:VC for list_rev"/>
<proof
prover="2"
prover="1"
timelimit="60"
memlimit="1000"
obsolete="false"
......@@ -448,7 +244,7 @@
<result status="valid" time="0.53"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="60"
memlimit="1000"
obsolete="false"
......@@ -456,7 +252,7 @@
<result status="valid" time="1.48"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -464,7 +260,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="60"
memlimit="1000"
obsolete="false"
......@@ -472,7 +268,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="60"
memlimit="1000"
obsolete="false"
......@@ -483,13 +279,13 @@
<goal
name="frame_model"
locfile="../list_rev.mlw"
loclnum="317" loccnumb="8" loccnume="19"
loclnum="319" loccnumb="8" loccnume="19"
sum="f985569418e176478a8130a3be94d5aa"
proved="true"
expanded="false"
shape="ainfix =amodelV0V1amodelamixfix [&lt;-]V0V2V3V1INain_ftV2alist_ftV0V1Iais_listV0V1Famodelamixfix [&lt;-]V0V2V3V1">
<proof
prover="4"
prover="3"
timelimit="10"
memlimit="0"
edited="list_rev_M2_frame_model_1.v"
......@@ -501,81 +297,25 @@
<goal
name="consistent_behv"
locfile="../list_rev.mlw"
loclnum="324" loccnumb="7" loccnume="22"
loclnum="326" loccnumb="7" loccnume="22"
sum="99bb383f09e67354ca8087f0d23f0c9b"
proved="false"
expanded="false"
expanded="true"
shape="fIais_listV0V2Iais_listV0V1F">
<proof
prover="0"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.10"/>
</proof>
<proof
prover="2"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="outofmemory" time="10.23"/>
</proof>
<proof
prover="3"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="59.77"/>
</proof>
<proof
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.14"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="59.68"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="59.63"/>
</proof>
</goal>
<goal
name="WP_parameter list_rev_behv"
locfile="../list_rev.mlw"
loclnum="327" loccnumb="6" loccnume="19"
loclnum="329" loccnumb="6" loccnume="19"
expl="VC for list_rev_behv"
sum="97f7bf1cdf1c1ac3fdba3dfaf94121ed"
sum="fda236352076285db244af93a7654bef"
proved="true"
expanded="true"
shape="iainfix =areverseamodelV1V0amodelV4V2Aais_listV4V2ainfix =areverseamodelV1V0ainfix ++areverseamodelV5V7amodelV5V6Aasep_list_listV5V7V6Aais_listV5V6Aais_listV5V7Iainfix =V7amixfix []V4V3FIainfix =V6V3FIainfix =V5amixfix [&lt;-]V4V3V2FNainfix =V3anullIainfix =areverseamodelV1V0ainfix ++areverseamodelV4V3amodelV4V2Aasep_list_listV4V3V2Aais_listV4V2Aais_listV4V3FAainfix =areverseamodelV1V0ainfix ++areverseamodelV1V0amodelV1anullAasep_list_listV1V0anullAais_listV1anullAais_listV1V0Iais_listV1V0FF">
expanded="false"
shape="iainfix =areverseamodelV1V0amodelV4V2Aais_listV4V2CfaNilainfix =V8amodelV5V7aConswVamodelV4V3Aainfix =areverseamodelV1V0ainfix ++areverseamodelV5V7amodelV5V6Aasep_list_listV5V7V6Aais_listV5V6Aais_listV5V7Iainfix =V7amixfix []V4V3FIainfix =V6V3FIainfix =V5amixfix [&lt;-]V4V3V2FNainfix =V3anullIainfix =areverseamodelV1V0ainfix ++areverseamodelV4V3amodelV4V2Aasep_list_listV4V3V2Aais_listV4V2Aais_listV4V3FAainfix =areverseamodelV1V0ainfix ++areverseamodelV1V0amodelV1anullAasep_list_listV1V0anullAais_listV1anullAais_listV1V0Iais_listV1V0FF">
<label
name="expl:VC for list_rev_behv"/>
<proof
prover="3"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="5.98"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -583,7 +323,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="60"
memlimit="1000"
obsolete="false"
......@@ -591,7 +331,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="60"
memlimit="1000"
obsolete="false"
......
examples/verifythis_fm2012_LRS/why3session.xml
View file @ 432af472
......@@ -623,14 +623,6 @@
archived="false">
<result status="timeout" time="4.99"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">