Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
024933ae
Commit
024933ae
authored
Feb 07, 2012
by
Jean-Christophe Filliâtre
Browse files
updated sessions on moloch
parent
1dceba24
Changes
4
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/programs/kmp/why3session.xml
View file @
024933ae
This diff is collapsed.
Click to expand it.
examples/programs/max_matrix/why3session.xml
View file @
024933ae
This diff is collapsed.
Click to expand it.
examples/programs/mergesort_list/why3session.xml
View file @
024933ae
...
...
@@ -4,16 +4,20 @@
name=
"examples/programs/mergesort_list/why3session.xml"
>
<prover
id=
"0"
prover_id=
"alt-ergo"
name=
"Alt-Ergo"
name=
"Alt-Ergo"
version=
"0.94"
/>
<prover
id=
"1"
prover_id=
"coq"
name=
"C
oq
"
version=
"
8.3pl3
"
/>
name=
"C
VC3
"
version=
"
2.2
"
/>
<prover
id=
"2"
prover_id=
"cvc3-2.2"
name=
"CVC3"
version=
"2.2"
/>
name=
"Coq"
version=
"8.3pl3"
/>
<prover
id=
"3"
name=
"Z3"
version=
"2.19"
/>
<file
name=
"../mergesort_list.mlw"
verified=
"true"
...
...
@@ -55,9 +59,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
...
...
@@ -75,9 +79,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.1
7
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.1
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -95,9 +99,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -115,9 +119,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -127,17 +131,56 @@
expl=
"parameter split"
sum=
"175c559ed497b5e2af30b9e02aca5175"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"CV3aNiltaConsVVapermutainfix ++V6V7ainfix ++V1ainfix ++V2V3Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6Iapermutainfix ++V6V7ainfix ++V2ainfix ++aConsV4V1V5Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6FIainfix =alengthaConsV4V1ainfix +alengthV2c1Oainfix =alengthaConsV4V1alengthV2Aainfix <alengthV5alengthV3Aainfix <=c0alengthV3Iainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFIainfix >=alengthV0c2F"
>
<label
name=
"expl:parameter split"
>
</label>
<proof
prover=
"2"
timelimit=
"20"
obsolete=
"false"
>
<result
status=
"valid"
time=
"3.49"
/>
</proof>
<transf
name=
"split_goal"
proved=
"true"
expanded=
"true"
>
<goal
name=
"WP_parameter split.5.0"
locfile=
"examples/programs/mergesort_list/../mergesort_list.mlw"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"11"
expl=
"parameter split"
sum=
"d66e5fe1179e30a6daf00f8ce32191ec"
proved=
"true"
expanded=
"false"
shape=
"CV3aNiltaConsVVainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6Iapermutainfix ++V6V7ainfix ++V2ainfix ++aConsV4V1V5Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6FIainfix =alengthaConsV4V1ainfix +alengthV2c1Oainfix =alengthaConsV4V1alengthV2Aainfix <alengthV5alengthV3Aainfix <=c0alengthV3Iainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFIainfix >=alengthV0c2F"
>
<label
name=
"expl:parameter split"
>
</label>
<proof
prover=
"0"
timelimit=
"10"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.00"
/>
</proof>
</goal>
<goal
name=
"WP_parameter split.5.1"
locfile=
"examples/programs/mergesort_list/../mergesort_list.mlw"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"11"
expl=
"parameter split"
sum=
"a2c261b7116a540bcfcca392ff34081c"
proved=
"true"
expanded=
"true"
shape=
"CV3aNiltaConsVVapermutainfix ++V6V7ainfix ++V1ainfix ++V2V3Iapermutainfix ++V6V7ainfix ++V2ainfix ++aConsV4V1V5Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6FIainfix =alengthaConsV4V1ainfix +alengthV2c1Oainfix =alengthaConsV4V1alengthV2Aainfix <alengthV5alengthV3Aainfix <=c0alengthV3Iainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFIainfix >=alengthV0c2F"
>
<label
name=
"expl:parameter split"
>
</label>
<proof
prover=
"3"
timelimit=
"10"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"1.88"
/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
...
...
@@ -148,7 +191,7 @@
expl=
"parameter merge"
sum=
"891111ea736658ed4790e0db98e650ae"
proved=
"true"
expanded=
"
tru
e"
expanded=
"
fals
e"
shape=
"CV1aConsVVCV0aConsVViainfix <=V4V2apermutaConsV4V6ainfix ++V0V1AasortedaConsV4V6IapermutV6ainfix ++V5V1AasortedV6FAasortedV1AasortedV5Aainfix <ainfix +alengthV5alengthV1ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1apermutaConsV2V7ainfix ++V0V1AasortedaConsV2V7IapermutV7ainfix ++V0V3AasortedV7FAasortedV3AasortedV0Aainfix <ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1aNilapermutV1ainfix ++V0V1AasortedV1aNilCV0aNilapermutV1ainfix ++V0V1AasortedV1wapermutV0ainfix ++V0V1AasortedV0IasortedV1AasortedV0FF"
>
<label
name=
"expl:parameter merge"
>
...
...
@@ -156,7 +199,7 @@
<transf
name=
"split_goal"
proved=
"true"
expanded=
"
tru
e"
>
expanded=
"
fals
e"
>
<goal
name=
"WP_parameter merge.1"
locfile=
"examples/programs/mergesort_list/../mergesort_list.mlw"
...
...
@@ -172,9 +215,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
4
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -190,11 +233,11 @@
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"
1.25
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"
0.77
"
/>
</proof>
</goal>
<goal
...
...
@@ -210,18 +253,18 @@
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
4
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
4
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -231,7 +274,7 @@
expl=
"parameter merge"
sum=
"97a0aa41004451e6280a9235311f9abc"
proved=
"true"
expanded=
"
tru
e"
expanded=
"
fals
e"
shape=
"CV1aConsVVCV0aConsVVapermutaConsV2V6ainfix ++V0V1AasortedaConsV2V6IapermutV6ainfix ++V0V3AasortedV6FIasortedV3AasortedV0Aainfix <ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1Iainfix <=V4V2NaNiltaNiltIasortedV1AasortedV0FF"
>
<label
name=
"expl:parameter merge"
>
...
...
@@ -239,7 +282,7 @@
<transf
name=
"split_goal"
proved=
"true"
expanded=
"
tru
e"
>
expanded=
"
fals
e"
>
<goal
name=
"WP_parameter merge.4.1"
locfile=
"examples/programs/mergesort_list/../mergesort_list.mlw"
...
...
@@ -253,10 +296,11 @@
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"30"
obsolete=
"false"
>
<result
status=
"valid"
time=
"3.72"
/>
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"2.53"
/>
</proof>
</goal>
<goal
...
...
@@ -266,17 +310,18 @@
expl=
"parameter merge"
sum=
"2b5c310fba2a3eda546fd55cd57701ef"
proved=
"true"
expanded=
"
tru
e"
expanded=
"
fals
e"
shape=
"CV1aConsVVCV0aConsVVapermutaConsV2V6ainfix ++V0V1IapermutV6ainfix ++V0V3AasortedV6FIasortedV3AasortedV0Aainfix <ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1Iainfix <=V4V2NaNiltaNiltIasortedV1AasortedV0FF"
>
<label
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
1
"
prover=
"
2
"
timelimit=
"10"
edited=
"mergesort_list_WP_M_WP_parameter_merge_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.69"
/>
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.51"
/>
</proof>
</goal>
</transf>
...
...
@@ -294,18 +339,18 @@
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
4
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -321,18 +366,18 @@
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
...
...
@@ -348,18 +393,18 @@
name=
"expl:parameter merge"
>
</label>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
4
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
</transf>
...
...
@@ -371,7 +416,7 @@
expl=
"parameter mergesort"
sum=
"148e580548bc6cea84a7a4fbe9649fdf"
proved=
"true"
expanded=
"
tru
e"
expanded=
"
fals
e"
shape=
"CV0aConswaNilOaNilapermutV0V0AasortedV0wapermutV5V0AasortedV5IapermutV5ainfix ++V3V4AasortedV5FAasortedV4AasortedV3IapermutV4V2AasortedV4FAainfix <alengthV2alengthV0Aainfix <=c0alengthV0IapermutV3V1AasortedV3FAainfix <alengthV1alengthV0Aainfix <=c0alengthV0IapermutV0ainfix ++V1V2Aainfix <=c1alengthV2Aainfix <=c1alengthV1FAainfix >=alengthV0c2F"
>
<label
name=
"expl:parameter mergesort"
>
...
...
@@ -379,7 +424,7 @@
<transf
name=
"split_goal"
proved=
"true"
expanded=
"
tru
e"
>
expanded=
"
fals
e"
>
<goal
name=
"WP_parameter mergesort.1"
locfile=
"examples/programs/mergesort_list/../mergesort_list.mlw"
...
...
@@ -395,9 +440,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
...
...
@@ -415,9 +460,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.
5
6"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.
4
6"
/>
</proof>
</goal>
<goal
...
...
@@ -435,9 +480,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -455,8 +500,8 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
...
...
@@ -475,9 +520,9 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
...
...
@@ -487,7 +532,7 @@
expl=
"parameter mergesort"
sum=
"2406d8c7ad1c339e9f3ec6f5928f2322"
proved=
"true"
expanded=
"
tru
e"
expanded=
"
fals
e"
shape=
"CV0aConswaNilOaNiltwapermutV5V0AasortedV5IapermutV5ainfix ++V3V4AasortedV5FIasortedV4AasortedV3IapermutV4V2AasortedV4FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0IapermutV3V1AasortedV3FIainfix <alengthV1alengthV0Aainfix <=c0alengthV0IapermutV0ainfix ++V1V2Aainfix <=c1alengthV2Aainfix <=c1alengthV1FIainfix >=alengthV0c2F"
>
<label
name=
"expl:parameter mergesort"
>
...
...
@@ -495,7 +540,7 @@
<transf
name=
"split_goal"
proved=
"true"
expanded=
"
tru
e"
>
expanded=
"
fals
e"
>
<goal
name=
"WP_parameter mergesort.6.1"
locfile=
"examples/programs/mergesort_list/../mergesort_list.mlw"
...
...
@@ -511,8 +556,8 @@
<proof
prover=
"0"
timelimit=
"10"
edi
te
d
=
""
obsolete
=
"false"
>
obsole
te=
"
false
"
archived
=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
...
...
@@ -523,17 +568,18 @@
expl=
"parameter mergesort"
sum=
"36d9f9d8488ec330229674873c02a8d7"
proved=
"true"
expanded=
"
tru
e"
expanded=
"
fals
e"
shape=
"CV0aConswaNilOaNiltwapermutV5V0IapermutV5ainfix ++V3V4AasortedV5FIasortedV4AasortedV3IapermutV4V2AasortedV4FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0IapermutV3V1AasortedV3FIainfix <alengthV1alengthV0Aainfix <=c0alengthV0IapermutV0ainfix ++V1V2Aainfix <=c1alengthV2Aainfix <=c1alengthV1FIainfix >=alengthV0c2F"
>
<label
name=
"expl:parameter mergesort"
>
</label>
<proof
prover=
"
1
"
prover=
"
2
"
timelimit=
"10"
edited=
"mergesort_list_WP_M_WP_parameter_mergesort_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.65"
/>
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.51"
/>
</proof>
</goal>
</transf>
...
...
examples/programs/vacid_0_sparse_array/why3session.xml
View file @
024933ae
This diff is collapsed.
Click to expand it.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment