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
6efd8df6
Commit
6efd8df6
authored
Feb 22, 2013
by
Jean-Christophe Filliâtre
Browse files
updated proof sessions (new check sums)
parent
1b1cd199
Changes
110
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/add_list/why3session.xml
View file @
6efd8df6
...
...
@@ -35,7 +35,7 @@
locfile=
"../add_list.mlw"
loclnum=
"32"
loccnumb=
"8"
loccnume=
"11"
expl=
"VC for sum"
sum=
"3
2888636214c7fa4e230bf82e6ac77a3
"
sum=
"3
a88e37519a95048cc50ef9138956651
"
proved=
"true"
expanded=
"true"
shape=
"CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF"
>
...
...
@@ -71,7 +71,7 @@
locfile=
"../add_list.mlw"
loclnum=
"44"
loccnumb=
"4"
loccnume=
"8"
expl=
"VC for main"
sum=
"
3a10ec75818cb1e12caf058f54c4a224
"
sum=
"
df005abc0acb54725806339e698597f8
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF"
>
...
...
@@ -106,7 +106,7 @@
locfile=
"../add_list.mlw"
loclnum=
"63"
loccnumb=
"4"
loccnume=
"7"
expl=
"VC for sum"
sum=
"
9a09cd5512c73c6f39d19ebad452bf9b
"
sum=
"
ba225088321d5a1a8cae0184cb19113d
"
proved=
"true"
expanded=
"true"
shape=
"itCV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FfIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F"
>
...
...
@@ -134,7 +134,7 @@
locfile=
"../add_list.mlw"
loclnum=
"86"
loccnumb=
"4"
loccnume=
"8"
expl=
"VC for main"
sum=
"
60c8394cd30207d93f17d7c3fedfc0e9
"
sum=
"
1cf88d24902cc9a993f7d1ddf27c27bf
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF"
>
...
...
examples/algo63/why3session.xml
View file @
6efd8df6
This diff is collapsed.
Click to expand it.
examples/algo64/why3session.xml
View file @
6efd8df6
...
...
@@ -28,7 +28,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"VC for quicksort"
sum=
"
c26bc5966c3e6167ba89ac93c22c1c44
"
sum=
"
b40455eea6fa8f5f8be3ae873ef4b885
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <V1V2asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Aapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FAainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Aainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Aapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FAainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Aainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FAainfix <V2V0Aainfix <V1V2Aainfix <=c0V1asorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -43,7 +43,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"1. precondition"
sum=
"a
d96be9342b2921e0685a3c71ef2641e
"
sum=
"a
45b02e8c4d56b83dd0ba0d355ebd5d3
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -63,7 +63,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"2. variant decrease"
sum=
"
c2762e2c2330783f29e00bd99138cf3d
"
sum=
"
0bf365deaa3a34ff3134bfbd740b2574
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -83,7 +83,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"3. precondition"
sum=
"
daf171ad4c114ee30fbbf1349d2b7807
"
sum=
"
185085aaf34ff7553db76e027b7b6ba4
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -103,7 +103,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"4. assertion"
sum=
"
51198e09ed8e178b882a49d8594b4e26
"
sum=
"
b21840d6e68ef9ac3f747096b12f348d
"
proved=
"true"
expanded=
"true"
shape=
"apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -123,7 +123,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"5. variant decrease"
sum=
"
50ec939b533e894dfb76caadddc061f7
"
sum=
"
810c5db5caf74579f3183df10554cfb4
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -143,7 +143,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"6. precondition"
sum=
"9
b87b4398347ac606d86452d7fde33dd
"
sum=
"9
7247797257b81988b838ad9002f4cf7
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -163,7 +163,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"7. assertion"
sum=
"
c15fe3f61dc8c59b3e1d38de7c034a0
0"
sum=
"
d410783d8fe90fe9ec9bae2f0952872
0"
proved=
"true"
expanded=
"true"
shape=
"apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -183,7 +183,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"8. postcondition"
sum=
"
07c91b9adda11c3ba9df6c29273f0a58
"
sum=
"
d7b340f2383cfa547f1ddddda332d682
"
proved=
"true"
expanded=
"true"
shape=
"apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -203,7 +203,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"9. postcondition"
sum=
"
1dc0e11fbb67f925ca616d57b5836c97
"
sum=
"
cc4da29a7cb4a6c9c850b3d63fa33ee2
"
proved=
"true"
expanded=
"true"
shape=
"asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -231,7 +231,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"10. postcondition"
sum=
"
ce4b3b1dc17f2b2a7f38c09b07e25546
"
sum=
"
6c0018c482239ff70d1707887727abac
"
proved=
"true"
expanded=
"true"
shape=
"apermut_subV3V3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -251,7 +251,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"11. postcondition"
sum=
"
acef80efe892965afead694a6b4d23
92"
sum=
"
2b9e560b9c4d73531e3e483336932d
92"
proved=
"true"
expanded=
"true"
shape=
"asorted_subV3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
examples/algo65/why3session.xml
View file @
6efd8df6
This diff is collapsed.
Click to expand it.
examples/alphaBeta/why3session.xml
View file @
6efd8df6
...
...
@@ -51,7 +51,7 @@
name=
"Test"
locfile=
"../alphaBeta.mlw"
loclnum=
"76"
loccnumb=
"7"
loccnume=
"11"
sum=
"
610608283a85bf303ebe1a84cfcfc086
"
sum=
"
af3ffdef718c759d4773bd79f43e7e30
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <=aprefix -aposition_valueado_moveV0V1aminmaxV0c1IamemV1V2Lalegal_movesV0F"
>
...
...
@@ -85,7 +85,7 @@
name=
"minmax_bound"
locfile=
"../alphaBeta.mlw"
loclnum=
"82"
loccnumb=
"8"
loccnume=
"20"
sum=
"
09da0270a2e52b38705869d9ac120b60
"
sum=
"
1bcd8a36394df0992b33bb260e348c88
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <aminmaxV0V1ainfinityAainfix <aprefix -ainfinityaminmaxV0V1Iainfix >=V1c0F"
>
...
...
@@ -103,7 +103,7 @@
name=
"minmax_nomove"
locfile=
"../alphaBeta.mlw"
loclnum=
"86"
loccnumb=
"8"
loccnume=
"21"
sum=
"
31d04b93aaada3edf39c7cebc00b7339
"
sum=
"
0b0addfda9118de4bafbe1a65e672cf1
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =aminmaxV0V1aposition_valueV0Iainfix =alegal_movesV0aNilAainfix >=V1c0F"
>
...
...
@@ -184,7 +184,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"VC for move_value_alpha_beta"
sum=
"
f2b2c50e29db1fb27fd1056697ca29b4
"
sum=
"
5eeda3672d8d2f2cd58191ef8c15dc40
"
proved=
"true"
expanded=
"false"
shape=
"iainfix <V6aprefix -V0Aainfix <aprefix -V1V6ainfix =aprefix -V5aprefix -V6iainfix <=V6aprefix -V1ainfix >=aprefix -V5V1ainfix <=aprefix -V5V0Laminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FAainfix >=ainfix -V3c1c0Iainfix >=V3c1F"
>
...
...
@@ -199,7 +199,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"1. precondition"
sum=
"a
2e31407b2d98a26cdc1eecfe67f4a18
"
sum=
"a
1808fdc345936478c7d217e8986f457
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=ainfix -V3c1c0Iainfix >=V3c1F"
>
...
...
@@ -275,7 +275,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"2. postcondition"
sum=
"
f7d37657adac949f80acee2dacdbf90
3"
sum=
"
8140eb9ce7909fb01a2e15bf334a887
3"
proved=
"true"
expanded=
"false"
shape=
"iainfix <V6aprefix -V0Aainfix <aprefix -V1V6ainfix =aprefix -V5aprefix -V6iainfix <=V6aprefix -V1ainfix >=aprefix -V5V1ainfix <=aprefix -V5V0Laminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F"
>
...
...
@@ -290,7 +290,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"1. postcondition"
sum=
"
3fe99f92c30fc7fdd5b8fa12275d56ad
"
sum=
"
4991642b458035aa4a6c7ff40583df8f
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =aprefix -V5aprefix -V6Iainfix <V6aprefix -V0Aainfix <aprefix -V1V6Laminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F"
>
...
...
@@ -310,7 +310,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"2. postcondition"
sum=
"
bce92f52b1606bc59d69750f380be885
"
sum=
"
2b8b8d3be5e8e6d388c3cbecd15a9cf9
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=aprefix -V5V1Iainfix <=V6aprefix -V1Iainfix <V6aprefix -V0Aainfix <aprefix -V1V6NLaminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F"
>
...
...
@@ -330,7 +330,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"3. postcondition"
sum=
"
8375fb15569dcaa7d79665539ccccad9
"
sum=
"
d98fbd0104c113af965c1a0969f25348
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <=aprefix -V5V0Iainfix <=V6aprefix -V1NIainfix <V6aprefix -V0Aainfix <aprefix -V1V6NLaminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F"
>
...
...
@@ -354,7 +354,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"VC for negabeta"
sum=
"
ff6c1977755082f26b247e1c0923a90b
"
sum=
"
e275db87e7bafa137960c3e485470254
"
proved=
"false"
expanded=
"true"
shape=
"iainfix =V3c0iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1Calegal_movesV2aNiliainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1aConsVViainfix >=V6V1iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V6aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V6V0ainfix >=V6V1iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V7aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V7V0ainfix >=V7V1Iiais_emptyV8ainfix =V7V6iainfix <V9V1Aainfix <amaxV6V0V9ainfix =V7V9iainfix <=V9amaxV6V0ainfix <=V7amaxV6V0ainfix >=V7V1LaminaTuple2V2V3V8LaelementsV5FAainfix >=V3c1Iiainfix <V10aprefix -V0Aainfix <aprefix -V1V10ainfix =V6aprefix -V10iainfix <=V10aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FAainfix >=V3c1Iainfix >=V3c0F"
>
...
...
@@ -369,7 +369,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"1. postcondition"
sum=
"
489e7cf3b79dacf889b72955ef519dc9
"
sum=
"
7cea8c16f45481393c7ed19323c9cf00
"
proved=
"true"
expanded=
"false"
shape=
"iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1Iainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -392,7 +392,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"1. postcondition"
sum=
"
465d551152bfe083b4fee0dc11e95459
"
sum=
"
e50fe264528ad54603548406e9bb093e
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =aposition_valueV2aminmaxV2V3Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Iainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -420,7 +420,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"2. postcondition"
sum=
"
1a4f137de291c168e659e30634529c12
"
sum=
"
a1e8321b9aa07cb6bd62c0dcf17267a6
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <=aposition_valueV2V0Iainfix <=aminmaxV2V3V0Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NIainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -448,7 +448,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"3. postcondition"
sum=
"
cccb5a149375a7097ef1ba22c3735228
"
sum=
"
3fe502381e5d642864ff4479130f67c4
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=aposition_valueV2V1Iainfix <=aminmaxV2V3V0NIainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NIainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -478,7 +478,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"2. postcondition"
sum=
"
da287b2b7c6c3f3b5b73c7588c08aec6
"
sum=
"
b0f71411555bf6f6a49319b10547e75d
"
proved=
"true"
expanded=
"false"
shape=
"Calegal_movesV2aNiliainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1aConsVVtIainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -493,7 +493,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"1. postcondition"
sum=
"
2d95f57ac8728f253948d1306cc076a2
"
sum=
"
bb8226faf0bc93acf933bd2038b98e23
"
proved=
"true"
expanded=
"false"
shape=
"Calegal_movesV2aNilainfix =aposition_valueV2aminmaxV2V3Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3aConsVVtIainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -529,7 +529,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"2. postcondition"
sum=
"
c2f4b25fea42605fc28196e65f9ebe7
6"
sum=
"
d180dc50e81f6bdf8edff0ae68aa5e8
6"
proved=
"true"
expanded=
"false"
shape=
"Calegal_movesV2aNilainfix <=aposition_valueV2V0Iainfix <=aminmaxV2V3V0Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NaConsVVtIainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -565,7 +565,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"3. postcondition"
sum=
"
a099e861a7b3c5ed07db90da336b1b54
"
sum=
"
c82d56a4ac016e8839dce0de84018fb8
"
proved=
"true"
expanded=
"false"
shape=
"Calegal_movesV2aNilainfix >=aposition_valueV2V1Iainfix <=aminmaxV2V3V0NIainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NaConsVVtIainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -603,7 +603,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"3. precondition"
sum=
"
cedb45baa8d038288ccd7521e119ddda
"
sum=
"
6045211f56a53ac4515749f51e289919
"
proved=
"true"
expanded=
"false"
shape=
"Calegal_movesV2aNiltaConsVVainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -639,7 +639,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"4. postcondition"
sum=
"
1e253830c031164ea76fdf61b7900f7c
"
sum=
"
640ab76cb472655ce8eaf23073fad568
"
proved=
"false"
expanded=
"true"
shape=
"Calegal_movesV2aNiltaConsVViainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V6aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V6V0ainfix >=V6V1Iainfix >=V6V1Iiainfix <V7aprefix -V0Aainfix <aprefix -V1V7ainfix =V6aprefix -V7iainfix <=V7aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -651,7 +651,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"5. precondition"
sum=
"
563184465ddec553604aa3248df427b9
"
sum=
"
1e74940031cdea274b38b37a1ddbefa6
"
proved=
"true"
expanded=
"false"
shape=
"Calegal_movesV2aNiltaConsVVainfix >=V3c1Iainfix >=V6V1NIiainfix <V7aprefix -V0Aainfix <aprefix -V1V7ainfix =V6aprefix -V7iainfix <=V7aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -687,7 +687,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"6. postcondition"
sum=
"
900c7b124ed942878c44afd849dadcf0
"
sum=
"
404e57d028647bc1a7aafe2ad331a326
"
proved=
"false"
expanded=
"true"
shape=
"Calegal_movesV2aNiltaConsVViainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V7aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V7V0ainfix >=V7V1Iiais_emptyV8ainfix =V7V6iainfix <V9V1Aainfix <amaxV6V0V9ainfix =V7V9iainfix <=V9amaxV6V0ainfix <=V7amaxV6V0ainfix >=V7V1LaminaTuple2V2V3V8LaelementsV5FIainfix >=V3c1Iainfix >=V6V1NIiainfix <V10aprefix -V0Aainfix <aprefix -V1V10ainfix =V6aprefix -V10iainfix <=V10aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F"
>
...
...
@@ -701,7 +701,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"VC for negabeta_rec"
sum=
"
0c0b2dedce3f81e08a8ab69099ccd44d
"
sum=
"
2134e39bfcf18e9393a818ff694e669f
"
proved=
"false"
expanded=
"true"
shape=
"CV5aNiliainfix <V7V1Aainfix <V0V7ainfix =V4V7iainfix <=V7V0ainfix <=V4V0ainfix >=V4V1LaminaTuple2V2V3V6Iais_emptyV6NLaelementsV5aConsVViainfix >=amaxV10V4V1iais_emptyV11ainfix =amaxV10V4V4iainfix <V12V1Aainfix <V0V12ainfix =amaxV10V4V12iainfix <=V12V0ainfix <=amaxV10V4V0ainfix >=amaxV10V4V1LaminaTuple2V2V3V11LaelementsV5iais_emptyV14ainfix =V13V4iainfix <V15V1Aainfix <V0V15ainfix =V13V15iainfix <=V15V0ainfix <=V13V0ainfix >=V13V1LaminaTuple2V2V3V14LaelementsV5Iiais_emptyV16ainfix =V13amaxV10V4iainfix <V17V1Aainfix <amaxamaxV10V4V0V17ainfix =V13V17iainfix <=V17amaxamaxV10V4V0ainfix <=V13amaxamaxV10V4V0ainfix >=V13V1LaminaTuple2V2V3V16LaelementsV9FAainfix >=V3c1Iiainfix <V18aprefix -V0Aainfix <aprefix -V1V18ainfix =V10aprefix -V18iainfix <=V18aprefix -V1ainfix >=V10V1ainfix <=V10V0Laminmaxado_moveV2V8ainfix -V3c1FAainfix >=V3c1Iainfix >=V3c1F"
>
...
...
@@ -716,7 +716,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"1. postcondition"
sum=
"
3588b2a391a2c2a894f03d0e0094ab00
"
sum=
"
1eb81ae3bdca869ea154b51098b87a86
"
proved=
"true"
expanded=
"false"
shape=
"CV5aNiliainfix <V7V1Aainfix <V0V7ainfix =V4V7iainfix <=V7V0ainfix <=V4V0ainfix >=V4V1LaminaTuple2V2V3V6Iais_emptyV6NLaelementsV5aConsVVtIainfix >=V3c1F"
>
...
...
@@ -736,7 +736,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"2. precondition"
sum=
"
2340cb631a5af087712eb69afbc6a0ba
"
sum=
"
9938059d21c1e699233305535f043a80
"
proved=
"true"
expanded=
"false"
shape=
"CV5aNiltaConsVVainfix >=V3c1Iainfix >=V3c1F"
>
...
...
@@ -756,7 +756,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"3. postcondition"
sum=
"
d35c091cedb5878157356798f59ed4db
"
sum=
"
5832ed2d4a603fa5e5e810fc8685468f
"
proved=
"false"
expanded=
"true"
shape=
"CV5aNiltaConsVViais_emptyV9ainfix =amaxV8V4V4iainfix <V10V1Aainfix <V0V10ainfix =amaxV8V4V10iainfix <=V10V0ainfix <=amaxV8V4V0ainfix >=amaxV8V4V1LaminaTuple2V2V3V9LaelementsV5Iainfix >=amaxV8V4V1Iiainfix <V11aprefix -V0Aainfix <aprefix -V1V11ainfix =V8aprefix -V11iainfix <=V11aprefix -V1ainfix >=V8V1ainfix <=V8V0Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1Iainfix >=V3c1F"
>
...
...
@@ -768,7 +768,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"4. precondition"
sum=
"
526d7164221d72a60befa04964995fdb
"
sum=
"
9eece8d8b9b26a3e2f91ba9a256d056e
"
proved=
"true"
expanded=
"false"
shape=
"CV5aNiltaConsVVainfix >=V3c1Iainfix >=amaxV8V4V1NIiainfix <V9aprefix -V0Aainfix <aprefix -V1V9ainfix =V8aprefix -V9iainfix <=V9aprefix -V1ainfix >=V8V1ainfix <=V8V0Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1Iainfix >=V3c1F"
>
...
...
@@ -788,7 +788,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"5. postcondition"
sum=
"
acc9956fd01105206f0bacf4e92622bb
"
sum=
"
67ad47c1bd49b82b563963e6cb5fa964
"
proved=
"false"
expanded=
"true"
shape=
"CV5aNiltaConsVViais_emptyV10ainfix =V9V4iainfix <V11V1Aainfix <V0V11ainfix =V9V11iainfix <=V11V0ainfix <=V9V0ainfix >=V9V1LaminaTuple2V2V3V10LaelementsV5Iiais_emptyV12ainfix =V9amaxV8V4iainfix <V13V1Aainfix <amaxamaxV8V4V0V13ainfix =V9V13iainfix <=V13amaxamaxV8V4V0ainfix <=V9amaxamaxV8V4V0ainfix >=V9V1LaminaTuple2V2V3V12LaelementsV7FIainfix >=V3c1Iainfix >=amaxV8V4V1NIiainfix <V14aprefix -V0Aainfix <aprefix -V1V14ainfix =V8aprefix -V14iainfix <=V14aprefix -V1ainfix >=V8V1ainfix <=V8V0Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1Iainfix >=V3c1F"
>
...
...
@@ -802,7 +802,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"161"
loccnumb=
"4"
loccnume=
"14"
expl=
"VC for alpha_beta"
sum=
"
5de2d33dad45be2736115fc2f77016e7
"
sum=
"
aefc65a0c9efa1dfbe91c46d1eb0a7e0
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V2aminmaxV0V1Iiainfix <aminmaxV0V1ainfinityAainfix <aprefix -ainfinityaminmaxV0V1ainfix =V2aminmaxV0V1iainfix <=aminmaxV0V1aprefix -ainfinityainfix <=V2aprefix -ainfinityainfix >=V2ainfinityFAainfix >=V1c0Iainfix >=V1c0F"
>
...
...
examples/arm/why3session.xml
View file @
6efd8df6
...
...
@@ -24,7 +24,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"VC for insertion_sort"
sum=
"
b316e30c82ef0fd3831a4b3ad8e0525d
"
sum=
"
3ce68aec817c9861b3b7cb459122b9e9
"
proved=
"false"
expanded=
"false"
shape=
"iainfix <=V5c10iainfix <agetV13V11agetV13ainfix -V11c1ainfix <V18V11Aainfix <=c0V11Aainfix <=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix <=V18V5Aainfix <=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11Aainfix <=c0V0FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1Aainfix <=c0V0FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V15ainfix +V12c1Fainfix <ainfix -c10V19ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix <=V19c11Aainfix <=c2V19Iainfix =V19ainfix +V5c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <=c0V0Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Aainfix <=c0V0Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -50,7 +50,7 @@
locfile=
"../arm.mlw"
loclnum=
"120"
loccnumb=
"6"
loccnume=
"18"
expl=
"VC for path_init_l2"
sum=
"
795f8de35a06a3c2af46ce51dec5f462
"
sum=
"
38759903d66d93a0badff4ab76c129e6
"
proved=
"true"
expanded=
"true"
shape=
"ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F"
>
...
...
@@ -78,7 +78,7 @@
locfile=
"../arm.mlw"
loclnum=
"127"
loccnumb=
"6"
loccnume=
"18"
expl=
"VC for path_l2_exit"
sum=
"
15ab5996d34e86896c649b5e2e7646ff
"
sum=
"
548a1717c3f91ea68d3cbefc909a77e8
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V0c9Iainfix =V4aFalseIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F"
>
...
...
examples/assigning_meanings_to_programs/why3session.xml
View file @
6efd8df6
...
...
@@ -24,7 +24,7 @@
locfile=
"../assigning_meanings_to_programs.mlw"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for sum"
sum=
"
ffd9a7dd39188363294776b2c47e64ce
"
sum=
"
778c6a7d6061eaf3c7f1c356d13dc553
"
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 <=c1V4FAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -51,7 +51,7 @@
locfile=
"../assigning_meanings_to_programs.mlw"
loclnum=
"38"
loccnumb=
"6"
loccnume=
"14"
expl=
"VC for division"
sum=
"
9bb49b04773111717366ff28ad1ed506
"
sum=
"
d1489af014bd44c27d427a8d972c2927
"
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 <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F"
>
...
...
examples/bellman_ford/why3session.xml
View file @
6efd8df6
This diff is collapsed.
Click to expand it.
examples/binary_search/why3session.xml
View file @
6efd8df6
...
...
@@ -24,7 +24,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"17"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"
7117980790d0ae65ea9a63dcdb93b30e
"
sum=
"
498abc049035c58ab372d0afa0f32a72
"
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 <=c0V4FAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FAainfix <=c0V0FF"
>
...
...
@@ -59,7 +59,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"60"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"
8bdc6aca362ddf7404a2f2d93ea218ed
"
sum=
"
bc045587c8509311b2f5f1930d15e6e0
"
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 <=c0V4FAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FAainfix <=c0V0FF"
>
...
...
@@ -86,7 +86,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"100"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"
5f760c6ff02952c3cb4e9c6699b517ad
"
sum=
"
6bcb889256f3f37a88157c5954e4de7e
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <=V4V3iainfix <agetV2V6V1ainfix <ainfix -V3V7ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V3Aainfix <=V7V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V7Iainfix =V7ainfix +V6c1FAainfix <=ainfix +V6c1amax_intAainfix <=amin_intainfix +V6c1iainfix >agetV2V6V1ainfix <ainfix -V9V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V9Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V9V0Aainfix <=c0V4Iainfix =V9ainfix -V6c1FAainfix <=ainfix -V6c1amax_intAainfix <=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <=V6V3Aainfix <=V4V6Lainfix +V4adivV5c2Aainfix <=ainfix +V4adivV5c2amax_intAainfix <=amin_intainfix +V4adivV5c2Lainfix -V3V4Aainfix <=ainfix -V3V4amax_intAainfix <=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix <V11V0Aainfix <=c0V11FIainfix <=V12V3Aainfix <=V4V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <V3V0Aainfix <=c0V4FAainfix <=V13ainfix -V0c1Aainfix <=c0V13Iainfix =agetV2V13V1Iainfix <V13V0Aainfix <=c0V13FAainfix <ainfix -V0c1V0Aainfix <=c0c0Aainfix <=ainfix -V0c1amax_intAainfix <=amin_intainfix -V0c1Iainfix <=agetV2V14agetV2V15Iainfix <V15V0Aainfix <=V14V15Aainfix <=c0V14FAainfix <=V0amax_intAainfix <=c0V0FF"
>
...
...
examples/binary_sqrt/why3session.xml
View file @
6efd8df6
...
...
@@ -24,7 +24,7 @@
locfile=
"../binary_sqrt.mlw"
loclnum=
"11"
loccnumb=
"10"
loccnume=
"14"
expl=
"VC for sqrt"
sum=
"
e08f528fae51036632b313fa55e111e7
"
sum=
"
4882bdabea8a2636d8e122a117a31162
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <c1.V1Aainfix <V0V1ainfix <V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix <=ainfix *c0.c0.V0ainfix <V0ainfix *ainfix +iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V1ainfix +iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V1Aainfix <=ainfix *iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V0Iainfix <V0ainfix *ainfix +V2ainfix *c2.V1ainfix +V2ainfix *c2.V1Aainfix <=ainfix *V2V2V0FAainfix <c0.ainfix *c2.V1Aainfix <=c0.V0Iainfix <c0.V1Aainfix <=c0.V0F"
>
...
...
@@ -39,7 +39,7 @@
locfile=
"../binary_sqrt.mlw"
loclnum=
"11"
loccnumb=
"10"
loccnume=
"14"
expl=
"1. postcondition"
sum=
"d
ff5fb4cc54d4ce8b3085bf8500cf886
"
sum=
"d
8ca659162fbee16af4ba06ea2838ed3
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix <=ainfix *c0.c0.V0Iainfix <c1.V1Aainfix <V0V1Iainfix <c0.V1Aainfix <=c0.V0F"
>
...
...
@@ -59,7 +59,7 @@
locfile=
"../binary_sqrt.mlw"
loclnum=
"11"
loccnumb=
"10"
loccnume=
"14"
expl=
"2. precondition"
sum=
"
a5829dc493992a85b515662d7f6094db
"
sum=
"
0e92423c222626d41e0be1057c52f22c
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <c0.ainfix *c2.V1Aainfix <=c0.V0Iainfix <c1.V1Aainfix <V0V1NIainfix <c0.V1Aainfix <=c0.V0F"
>
...
...
@@ -79,7 +79,7 @@
locfile=
"../binary_sqrt.mlw"
loclnum=
"11"
loccnumb=
"10"
loccnume=
"14"
expl=
"3. postcondition"
sum=
"
e6eafff38a2ee8e8809732d3ebe73f6b
"
sum=
"
319c1af1043efe665bef4b068ab0986c
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <V0ainfix *ainfix +iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V1ainfix +iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V1Aainfix <=ainfix *iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V0Iainfix <V0ainfix *ainfix +V2ainfix *c2.V1ainfix +V2ainfix *c2.V1Aainfix <=ainfix *V2V2V0FIainfix <c0.ainfix *c2.V1Aainfix <=c0.V0Iainfix <c1.V1Aainfix <V0V1NIainfix <c0.V1Aainfix <=c0.V0F"
>
...
...
examples/bitvectors/bitvector/why3session.xml
View file @
6efd8df6
...
...
@@ -37,13 +37,13 @@
name=
"BitVector"
locfile=
"../bitvector.why"
loclnum=
"3"
loccnumb=
"7"
loccnume=
"16"
verified=
"
tru
e"
verified=
"
fals
e"
expanded=
"true"
>
<goal
name=
"Nth_bw_xor_v1true"
locfile=
"../bitvector.why"
loclnum=
"46"
loccnumb=
"8"
loccnume=
"25"
sum=
"
10f5b792bf582463d0d58e59cf9fa4a6
"
sum=
"
8ab21ecf98d452f541b8eb7d5124b37e
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthabw_xorV0V1V2anotbanthV1V2Iainfix =anthV0V2aTrueAainfix <V2asizeAainfix <=c0V2F"
>
...
...
@@ -76,7 +76,7 @@
name=
"Nth_bw_xor_v1false"
locfile=
"../bitvector.why"
loclnum=
"50"
loccnumb=
"8"
loccnume=
"26"
sum=
"
442c811ba72eb92d69b94d13448101e2
"
sum=
"
9d3506cc5d507b27ef36c21e64c6f394
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthabw_xorV0V1V2anthV1V2Iainfix =anthV0V2aFalseAainfix <V2asizeAainfix <=c0V2F"
>
...
...
@@ -101,7 +101,7 @@
name=
"Nth_bw_xor_v2true"
locfile=
"../bitvector.why"
loclnum=
"54"
loccnumb=
"8"
loccnume=
"25"
sum=
"
0316258b63daca705db40006d2c64ee9
"
sum=
"
a1c444f056510ff60acc685ce74fde7e
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthabw_xorV0V1V2anotbanthV0V2Iainfix =anthV1V2aTrueAainfix <V2asizeAainfix <=c0V2F"
>
...
...
@@ -134,7 +134,7 @@
name=
"Nth_bw_xor_v2false"
locfile=
"../bitvector.why"
loclnum=
"58"
loccnumb=
"8"
loccnume=
"26"
sum=
"b
4ce040bc55e95fb610ab1970a7cca10
"
sum=
"b
c8a7c4bde80c78261e3eff1c91e2d53
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthabw_xorV0V1V2anthV0V2Iainfix =anthV1V2aFalseAainfix <V2asizeAainfix <=c0V2F"
>
...
...
@@ -167,7 +167,7 @@
name=
"to_nat_of_zero2"
locfile=
"../bitvector.why"
loclnum=
"194"
loccnumb=
"8"
loccnume=
"23"
sum=
"
dc229a800f0688a2b4561091bf098e5c
"
sum=
"
f9ed7782c61d349a69282b399dc5a228
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =ato_nat_subV0V2c0ato_nat_subV0V1c0Iainfix =anthV0V3aFalseIainfix >V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >=V2V1Aainfix >asizeV2F"
>
...
...
@@ -185,7 +185,7 @@
name=
"to_nat_of_zero"
locfile=
"../bitvector.why"
loclnum=
"200"
loccnumb=
"8"
loccnume=
"22"
sum=
"
db21f52ebbdce5d68f7ade7bab22eb49
"
sum=
"
b9471b6011def335b16c605f8147f11b
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =ato_nat_subV0V2V1c0Iainfix =anthV0V3aFalseIainfix >=V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >asizeV2F"
>
...
...
@@ -203,8 +203,8 @@
name=
"to_nat_of_one"
locfile=
"../bitvector.why"
loclnum=
"205"
loccnumb=
"8"
loccnume=
"21"
sum=
"
d0f3f334ff9aa4208fcb9275bed58700
"
proved=
"
tru
e"
sum=
"
8e2f700b9033bfa63444ee9755e06202
"
proved=
"
fals
e"
expanded=
"false"
shape=
"ainfix =ato_nat_subV0V2V1ainfix -apow2ainfix +ainfix -V2V1c1c1Iainfix =anthV0V3aTrueIainfix >=V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >=V2V1Aainfix >asizeV2F"
>
<proof
...
...
@@ -214,14 +214,14 @@
edited=
"bitvector_BitVector_to_nat_of_one_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
valid
"
time=
"
2.3
3"
/>
<result
status=
"
unknown
"
time=
"
1.2
3"
/>
</proof>
</goal>
<goal
name=
"to_nat_sub_footprint"
locfile=
"../bitvector.why"
loclnum=
"210"
loccnumb=
"8"
loccnume=
"28"
sum=
"
eb64885d450d92719446175647ecd865
"
sum=
"
f7ad8a1b804f5129eb5f1963f56b8e14
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =ato_nat_subV0V2V3ato_nat_subV1V2V3Iainfix =anthV0V4anthV1V4Iainfix <=V4V2Aainfix <=V3V4FIainfix >=V3c0Aainfix >asizeV2F"
>
...
...
@@ -239,7 +239,7 @@
name=
"nth_from_int_low_even"
locfile=
"../bitvector.why"
loclnum=
"297"
loccnumb=
"8"
loccnume=
"29"
sum=
"
6ff9d16523adfad9200eb17620c479e4
"
sum=
"
87e232d48297d2cad90e7c7f4ce774a9
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthafrom_intV0c0aFalseIainfix =amodV0c2c0F"
>
...
...
@@ -272,7 +272,7 @@
name=
"nth_from_int_low_odd"
locfile=
"../bitvector.why"
loclnum=
"300"
loccnumb=
"8"
loccnume=
"28"
sum=
"c
95f783131bf812ebf23e03e889dd4f7
"
sum=
"c
a17f2b1f131e93c5e2bfe678f0a8a84
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthafrom_intV0c0aTrueIainfix =amodV0c2c0NF"
>
...
...
@@ -305,7 +305,7 @@
name=
"nth_from_int_0"
locfile=
"../bitvector.why"
loclnum=
"303"
loccnumb=
"8"
loccnume=
"22"
sum=
"
450e9ffc38f29b601de72ca9bf764349
"
sum=
"
e6c43852eba46f88d3880bac4d50fc76
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthafrom_intc0V0aFalseIainfix >=V0c0Aainfix >asizeV0F"
>
...
...
@@ -338,7 +338,7 @@
name=
"nth_from_int2c_low_even"
locfile=
"../bitvector.why"
loclnum=
"339"
loccnumb=
"8"
loccnume=
"31"
sum=
"
a67e28f685d8c01377cf3c72e4533960
"
sum=
"
b79d2cc77be2fe002c6d949b7e7f787d
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0F"
>
...
...
@@ -371,7 +371,7 @@
name=
"nth_from_int2c_low_odd"
locfile=
"../bitvector.why"
loclnum=
"342"
loccnumb=
"8"
loccnume=
"30"
sum=
"a
7d2a84135931c151cd1
69
a
d5
25f2f3f
"
sum=
"a
0b8dc60aa4a1c336b44f5b3ccc
69
f
d5"