Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
3c180f29
Commit
3c180f29
authored
Oct 27, 2011
by
MARCHE Claude
Browse files
update sessions
parent
5dd7b133
Changes
46
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/check-builtin/bool/why3session.xml
View file @
3c180f29
...
...
@@ -56,7 +56,7 @@
expanded=
"true"
>
<goal
name=
"G1"
sum=
"9
d7c94235f7897fd905a8556b0233fc3
"
sum=
"9
69c403f9c22509f17918ed3d3b37bd2
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =aTrueaFalseN"
>
...
...
@@ -72,7 +72,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
<proof
prover=
"z3"
...
...
@@ -86,12 +86,12 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
name=
"G2"
sum=
"
36ea15fbd463bb8c515283a060144275
"
sum=
"
78a2bf185ba7da8e25d94706bbd9c161
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V0aFalseOainfix =V0aTrueF"
>
...
...
@@ -107,7 +107,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
<proof
prover=
"z3"
...
...
@@ -126,7 +126,7 @@
</goal>
<goal
name=
"G3"
sum=
"
890f0a91dd5486dd2c466c6ff73ca3f9
"
sum=
"
a0bc68bb0d3f237c6ad0611e98d62612
"
proved=
"true"
expanded=
"true"
shape=
"fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF"
>
...
...
@@ -156,7 +156,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
</theory>
...
...
examples/genealogy/why3session.xml
View file @
3c180f29
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name=
"
.
/genealogy/why3session.xml"
>
name=
"
examples
/genealogy/why3session.xml"
>
<prover
id=
"alt-ergo"
name=
"Alt-Ergo"
...
...
@@ -65,7 +65,7 @@
timelimit=
"3"
edited=
""
obsolete=
"false"
>
<result
status=
"unknown"
time=
"0.0
1
"
/>
<result
status=
"unknown"
time=
"0.0
2
"
/>
</proof>
<proof
prover=
"cvc3"
...
...
@@ -128,7 +128,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
<proof
prover=
"eprover"
...
...
@@ -198,14 +198,14 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"yices"
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
3
"
/>
</proof>
<proof
prover=
"vampire"
...
...
@@ -240,14 +240,14 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"eprover"
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"z3"
...
...
@@ -261,21 +261,21 @@
timelimit=
"3"
edited=
""
obsolete=
"false"
>
<result
status=
"
timeout
"
time=
"3.0
1
"
/>
<result
status=
"
unknown
"
time=
"3.0
8
"
/>
</proof>
<proof
prover=
"yices"
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
4
"
/>
</proof>
<proof
prover=
"spass"
timelimit=
"3"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"3.
63
"
/>
<result
status=
"timeout"
time=
"3.
55
"
/>
</proof>
</goal>
<goal
...
...
@@ -352,7 +352,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"eprover"
...
...
@@ -387,7 +387,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -415,21 +415,21 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
<proof
prover=
"z3"
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
<proof
prover=
"vampire"
timelimit=
"3"
edited=
""
obsolete=
"false"
>
<result
status=
"
timeout
"
time=
"
3.01
"
/>
<result
status=
"
unknown
"
time=
"
2.97
"
/>
</proof>
<proof
prover=
"yices"
...
...
@@ -443,7 +443,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
</theory>
...
...
examples/hoare_logic/formula/why3session.xml
View file @
3c180f29
...
...
@@ -9,7 +9,7 @@
<prover
id=
"coq"
name=
"Coq"
version=
"8.
2
pl
1
"
/>
version=
"8.
3
pl
2
"
/>
<prover
id=
"cvc3"
name=
"CVC3"
...
...
@@ -61,7 +61,7 @@
expanded=
"true"
>
<goal
name=
"Test1"
sum=
"
ad0268b5331a68e8313850369f12a695
"
sum=
"
e329e8a4a6efb1ac7341b8e1c61a6554
"
proved=
"true"
expanded=
"true"
shape=
"Lamk_identc0LasetaconstaFalseV0aTrueainfix =aevalaForaFnotaFatomV0aFfalseV1aFalse"
>
...
...
@@ -70,7 +70,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"alt-ergo"
...
...
@@ -84,7 +84,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.
24
"
/>
<result
status=
"valid"
time=
"0.
19
"
/>
</proof>
</goal>
</theory>
...
...
examples/hoare_logic/wp/why3session.xml
View file @
3c180f29
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name=
"wp/why3session.xml"
>
name=
"
examples/hoare_logic/
wp/why3session.xml"
>
<prover
id=
"alt-ergo"
name=
"Alt-Ergo"
...
...
@@ -9,7 +9,7 @@
<prover
id=
"coq"
name=
"Coq"
version=
"8.
2
pl
1
"
/>
version=
"8.
3
pl
2
"
/>
<prover
id=
"cvc3"
name=
"CVC3"
...
...
@@ -93,7 +93,7 @@
timelimit=
"5"
edited=
"wp_Imp_Test55_2.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.5
2
"
/>
<result
status=
"valid"
time=
"0.5
0
"
/>
</proof>
</goal>
<goal
...
...
@@ -135,7 +135,7 @@
timelimit=
"5"
edited=
"wp_Imp_If42_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.
82
"
/>
<result
status=
"valid"
time=
"0.
79
"
/>
</proof>
</goal>
<goal
...
...
examples/programs/assigning_meanings_to_programs/why3session.xml
View file @
3c180f29
...
...
@@ -57,7 +57,7 @@
<goal
name=
"WP_parameter sum"
expl=
"parameter sum"
sum=
"
4140091742c46acee6f869ae678e559b
"
sum=
"
623e0f9ea6fbf22e855f3e4465a61e44
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF"
>
...
...
@@ -66,7 +66,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
</theory>
...
...
@@ -77,7 +77,7 @@
<goal
name=
"WP_parameter division"
expl=
"parameter division"
sum=
"
719f7e3611b91d4d380d1c5aaeccfd4c
"
sum=
"
1fd6f117a9ecb1227e7acde6a58e5f39
"
proved=
"true"
expanded=
"true"
shape=
"iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF"
>
...
...
examples/programs/binary_search/why3session.xml
View file @
3c180f29
...
...
@@ -57,7 +57,7 @@
<goal
name=
"WP_parameter binary_search"
expl=
"parameter binary_search"
sum=
"
50b8c872166cdcf1ce62c180623e0cd9
"
sum=
"
2d4368f5fd910b1ceb69adef571ead55
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF"
>
...
...
@@ -66,7 +66,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
3
"
/>
</proof>
<proof
prover=
"z3"
...
...
@@ -84,7 +84,7 @@
<goal
name=
"WP_parameter binary_search"
expl=
"parameter binary_search"
sum=
"d
076677e78d6d426049b9324eeed421e
"
sum=
"d
5cd94966f7526a19692c7d56b842e9f
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <=V4V3iainfix <agetV2V5V1ainfix <ainfix -V3V6ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V7V3Aainfix <=V6V7Iainfix =agetV2V7V1Iainfix <V7V0Aainfix <=c0V7FAainfix <V3V0Aainfix <=c0V6Iainfix =V6ainfix +V5c1Fiainfix >agetV2V5V1ainfix <ainfix -V8V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V9V8Aainfix <=V4V9Iainfix =agetV2V9V1Iainfix <V9V0Aainfix <=c0V9FAainfix <V8V0Aainfix <=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Iainfix <=V5V3Aainfix <=V4V5FAainfix <=V4V3ainfix =agetV2V10V1NIainfix <V10V0Aainfix <=c0V10FIainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FFFF"
>
...
...
examples/programs/bresenham/why3session.xml
View file @
3c180f29
...
...
@@ -56,7 +56,7 @@
expanded=
"true"
>
<goal
name=
"invariant_is_ok"
sum=
"
86594dd0d50f484f3737ddf51df6b48e
"
sum=
"
519834903610d859bd7dac5b2a044f72
"
proved=
"true"
expanded=
"true"
shape=
"abestV0V1Iainvariant_V0V1V2F"
>
...
...
@@ -65,13 +65,13 @@
timelimit=
"10"
edited=
"bresenham_WP_M_invariant_is_ok_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"1.2
2
"
/>
<result
status=
"valid"
time=
"1.2
8
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter bresenham"
expl=
"parameter bresenham"
sum=
"
f60a88f9babd662203811e119f193488
"
sum=
"
d99ea3e7abed5f54b1851cd4812c367c
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0"
>
...
...
@@ -82,7 +82,7 @@
<goal
name=
"WP_parameter bresenham.1"
expl=
"loop invariant init"
sum=
"
b5a81c756dcc145ce2d22b88b12a50ba
"
sum=
"
4b176b3ddb9ce2f3a36d8720e5105450
"
proved=
"true"
expanded=
"true"
shape=
"ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0"
>
...
...
@@ -111,7 +111,7 @@
<goal
name=
"WP_parameter bresenham.2"
expl=
"assertion"
sum=
"
02807
33
9
18
becad4a00f65e5b573f8b7
"
sum=
"
e
3318
304367051f407802ab6b94e9853
"
proved=
"true"
expanded=
"true"
shape=
"abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"
>
...
...
@@ -133,7 +133,7 @@
<goal
name=
"WP_parameter bresenham.3"
expl=
"loop invariant preservation"
sum=
"
9804176574e7b0b0562a2675bee121cf
"
sum=
"
d442f459cee038e5fb402ae383f95758
"
proved=
"true"
expanded=
"true"
shape=
"ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"
>
...
...
@@ -155,7 +155,7 @@
<goal
name=
"WP_parameter bresenham.4"
expl=
"loop variant decreases"
sum=
"
19afbdf269f0d3861532dc1c0db1be4
d"
sum=
"
bf9395eb9f3d806eae0d394a85dc935
d"
proved=
"true"
expanded=
"true"
shape=
"ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"
>
...
...
@@ -164,7 +164,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"alt-ergo"
...
...
@@ -184,7 +184,7 @@
<goal
name=
"WP_parameter bresenham.5"
expl=
"loop invariant preservation"
sum=
"
e2c7f84e17390a5914561f4260af95ce
"
sum=
"
b3ddc7bdbce5b6f6493f6207a24d5539
"
proved=
"true"
expanded=
"true"
shape=
"ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"
>
...
...
@@ -206,7 +206,7 @@
<goal
name=
"WP_parameter bresenham.6"
expl=
"loop variant decreases"
sum=
"
023a9d00567ec555ea12e968d0d095e7
"
sum=
"
c2ccf4c036b64b2f8ed018313e27652b
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"
>
...
...
@@ -215,7 +215,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
<proof
prover=
"alt-ergo"
...
...
examples/programs/checking_a_large_routine/why3session.xml
View file @
3c180f29
...
...
@@ -57,7 +57,7 @@
<goal
name=
"WP_parameter routine"
expl=
"parameter routine"
sum=
"
8d67dd8989bfbff7b9aa8fd6b3331f2b
"
sum=
"
e9943b170f7bb3699ce2bcd677d1c8df
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <V2V0iainfix <=V3V2ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1Fainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV7Aainfix <=V7V0Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix =V1afactV0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F"
>
...
...
@@ -68,7 +68,7 @@
<goal
name=
"WP_parameter routine.1"
expl=
"loop invariant init"
sum=
"
6bce3725f9d5cb993d5a78588a93f5e4
"
sum=
"
cf4d4ec6d860d93ad83a718703abfdf6
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F"
>
...
...
@@ -77,13 +77,13 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter routine.2"
expl=
"loop invariant init"
sum=
"
96abc74f3d7de438d484e86d23209e71
"
sum=
"
c8674b048553d8e22c93a2121e9547ee
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"
>
...
...
@@ -98,7 +98,7 @@
<goal
name=
"WP_parameter routine.3"
expl=
"loop invariant preservation"
sum=
"
a8c507b1d2ed8ec61759d40f1153bfa9
"
sum=
"
bd00fd1d7ba80e558d08e48ba1f00300
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"
>
...
...
@@ -113,7 +113,7 @@
<goal
name=
"WP_parameter routine.4"
expl=
"loop variant decreases"
sum=
"
d6b7c71c61fb2329c082beec15c1375b
"
sum=
"
51d4291be664900c9cbd81c003133093
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"
>
...
...
@@ -128,7 +128,7 @@
<goal
name=
"WP_parameter routine.5"
expl=
"loop invariant preservation"
sum=
"
525d66fa570db0f594598f5823cd34de
"
sum=
"
913719957de4bd9785c5691c0e30d026
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"
>
...
...
@@ -143,7 +143,7 @@
<goal
name=
"WP_parameter routine.6"
expl=
"loop variant decreases"
sum=
"
22f5ce05a2d1a524ac6b20dd45232e4c
"
sum=
"
c6d17a46365b163d54d0b27a82a0bf93
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"
>
...
...
@@ -158,7 +158,7 @@
<goal
name=
"WP_parameter routine.7"
expl=
"normal postcondition"
sum=
"
b309acf5ab5ec6946742d21c98a6f9d9
"
sum=
"
f6f36c963637e7834456ced524a93c7c
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1afactV0Iainfix <V2V0NIainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"
>
...
...
@@ -167,7 +167,7 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
</transf>
...
...
@@ -175,7 +175,7 @@
<goal
name=
"WP_parameter routine2"
expl=
"parameter routine2"
sum=
"
9f34d7541a7bf8683baab7309cae8ff7
"
sum=
"
23a788ebffdb3b8b2ffa0b34431e1c13
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1Aainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFAainfix =c1afactc0Iainfix <=c0ainfix -V0c1Aainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F"
>
...
...
@@ -186,7 +186,7 @@
<goal
name=
"WP_parameter routine2.1"
expl=
"normal postcondition"
sum=
"
41eaebc80e139a72d2123360409d7ff7
"
sum=
"
05b73de596d62510f46cb9c8fa84d31e
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F"
>
...
...
@@ -201,7 +201,7 @@
<goal
name=
"WP_parameter routine2.2"
expl=
"for loop initialization"
sum=
"
d39a2112bcf2ccc4b49be3f59819918
3"
sum=
"
45ce46675e3ae2bd664fb071fb218ec
3"
proved=
"true"
expanded=
"true"
shape=
"ainfix =c1afactc0Iainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
...
...
@@ -216,7 +216,7 @@
<goal
name=
"WP_parameter routine2.3"
expl=
"for loop preservation"
sum=
"
acbcde2a8d488f1eeb61420d1b3f35f2
"
sum=
"
d40b8c6ef80176abf3f3eba6a6f85c76
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
...
...
@@ -225,13 +225,13 @@
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
3
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter routine2.4"
expl=
"normal postcondition"
sum=
"
1efcca2176899eb08342b2ff44429dfd
"
sum=
"
5f544f2aeadc86cd3c1aeea6d40bdbe3
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1FIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
...
...
examples/programs/edit_distance/why3session.xml
View file @
3c180f29
This diff is collapsed.
Click to expand it.
examples/programs/euler001/why3session.xml
View file @
3c180f29
...
...
@@ -65,7 +65,7 @@
timelimit=
"5"
edited=
"euler001_DivModHints_mod_div_unique_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.5
2
"
/>
<result
status=
"valid"
time=
"0.5
3
"
/>
</proof>
</goal>
<goal
...
...
@@ -93,7 +93,7 @@
timelimit=
"5"
edited=
"euler001_DivModHints_mod_succ_2_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.6
1
"
/>
<result
status=
"valid"
time=
"0.6
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -121,7 +121,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.3
5
"
/>
<result
status=
"valid"
time=
"0.3
4
"
/>
</proof>
<proof
prover=
"cvc3"
...
...
@@ -135,7 +135,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.1
5
"
/>
<result
status=
"valid"
time=
"0.1
4
"
/>
</proof>
</goal>
</theory>
...
...
@@ -161,7 +161,7 @@
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.2
4
"
/>
<result
status=
"valid"
time=
"0.2
5
"
/>
</proof>
<proof
prover=
"z3"
...
...
@@ -196,7 +196,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"5.0
2
"
/>
<result
status=
"timeout"
time=
"5.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -210,7 +210,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"5.0
2
"
/>
<result
status=
"timeout"
time=
"5.0
1
"
/>
</proof>
<proof
prover=
"alt-ergo"
...
...
@@ -224,7 +224,7 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"5.
0
2"
/>
<result
status=
"timeout"
time=
"5.2
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -238,21 +238,21 @@
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.6
7
"
/>
<result
status=
"valid"
time=
"0.6
6
"
/>
</proof>
<proof
prover=
"cvc3"
timelimit=
"5"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.7
4
"
/>
<result
status=
"valid"
time=
"0.7
3
"
/>
</proof>
<proof
prover=
"z3"