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
59cecc21
Commit
59cecc21
authored
Mar 08, 2013
by
Jean-Christophe Filliâtre
Browse files
updated proof sesssions, fixed one proof
parent
ffb47c11
Changes
128
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/add_list/why3session.xml
View file @
59cecc21
...
...
@@ -35,7 +35,7 @@
locfile=
"../add_list.mlw"
loclnum=
"32"
loccnumb=
"8"
loccnume=
"11"
expl=
"VC for sum"
sum=
"
b655fa25e271e649aca23e9cc43dddcd
"
sum=
"
98a5545af1ab7e2f135821ad2fe70910
"
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=
"
47f3e40b493f519ebf1c4be2f438d08a
"
sum=
"
127fcdeab244cfbe4aec7fce6fdb7015
"
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=
"c4
1dd4b709a78980ecafa56e520f250b
"
sum=
"
1
c4
542683e081bd2f3c3310ee00d1644
"
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=
"
d6d5b03ee7f7b7855cd1135a9c87ab0e
"
sum=
"
80a39093aaa0fa258939e15895a7ebf1
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF"
>
...
...
examples/algo63/why3session.xml
View file @
59cecc21
This diff is collapsed.
Click to expand it.
examples/algo64/why3session.xml
View file @
59cecc21
...
...
@@ -28,7 +28,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"VC for quicksort"
sum=
"
5bad16d0f07bc4f66c98b988f2fd73a7
"
sum=
"
ab2a63ccffd01ef10ebb7dc0e7571df9
"
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=
"
78ff0ba8a03ecb4552b6894224928cf3
"
sum=
"
14d442b4820bcd8a9b4451df6a4b26b0
"
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=
"
1a2d41703fab4faaeb527dbf69806fdc
"
sum=
"
baaff721097293a6b7300bf2ebadade8
"
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=
"
5c4469adf46d4939a3813d207849f75d
"
sum=
"
d75ab7d682afc5e6ce4fcecba4b6b9bf
"
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=
"
235590bf66c96bcffc40647251ca8e7a
"
sum=
"
a5d2ec75c570aab7ea1d4214627ec136
"
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=
"
ac836f8d3f086054674e4c60090520a9
"
sum=
"
c3367cf5d49eba7c5470313bd16c122a
"
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=
"
6546b46be7267386af528de814800fc2
"
sum=
"
c28c61c377b86f8f567e7faa06beb325
"
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=
"
75c69e76e7f0c4a831886e9b503d9edd
"
sum=
"
3a8a5f4370467868497a7044ff8b4b14
"
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=
"
be21a4eeb36482399f92dac7cbe0c767
"
sum=
"
993ac877509f5322a1f21b7ea6ee0b88
"
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=
"
706b3fda811fd7a432ec6d58ceb01363
"
sum=
"
de7baf4df5c0adb5ede8feab3eec1f5d
"
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=
"
3b9cbe2d79bcac592f3dffca6673485
2"
sum=
"
ed3209cafe36a6b310b180fc021fac8
2"
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=
"
3b968c1dc9bf57ac80fd52b1a6edcfd7
"
sum=
"
8239ff0463764f17dfdff17f3552b48c
"
proved=
"true"
expanded=
"true"
shape=
"asorted_subV3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
examples/algo65/why3session.xml
View file @
59cecc21
This diff is collapsed.
Click to expand it.
examples/alphaBeta/why3session.xml
View file @
59cecc21
...
...
@@ -51,7 +51,7 @@
name=
"Test"
locfile=
"../alphaBeta.mlw"
loclnum=
"76"
loccnumb=
"7"
loccnume=
"11"
sum=
"
1aa960b887d5af278444d89cef166c30
"
sum=
"
85fb955fbb86dc0b3ce18c39a8487a47
"
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=
"
a3fe8ad5d354c07f77310e49bed57baa
"
sum=
"
9cfaeb65c5d3139897dbe65f58e3e115
"
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=
"3
7f686764a137ef6323e22e3c1c89384
"
sum=
"3
f57c373dd7bffe014c0fc7379bfb061
"
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=
"
e4c492a0ec689b1462b839b1b894fc8c
"
sum=
"
d59d0820791b22bd64c71122b52dbed6
"
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=
"
53a92003b802c519c4f3df9e61415222
"
sum=
"
6c771a70f3772fc0de83166df0726e41
"
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=
"
1b451dfd562ff0261baabe943dd22f7c
"
sum=
"
4f664110919b05b7c0cd07194f95ed2a
"
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=
"
c652eed1e2f439d45f47ef23627c75ae
"
sum=
"
2622fb2ccc85199e88b50f317413eafc
"
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=
"
84638a48ccdaf2d8b6340da57fb5434c
"
sum=
"
d12c0dd1ecd1107b6a2d679df062bf5e
"
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=
"
83052a9bb2fb4c57bd268f4c476f41d2
"
sum=
"
b8127b1086c13ce45cd041422c18bafa
"
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=
"
9d7bfdbcc42fc5c7cec3abfcab211367
"
sum=
"
3ce516f9995e5ac64fabf6df66d3b0de
"
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=
"
ab8681aaf4912bba2f99a0ed984911d9
"
sum=
"
8e218d47e74e6cdb48feeae240f862b8
"
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=
"
bd104fc8c08908b07ef8a9484e57a399
"
sum=
"
8ee9657dfb70729d16a084dbedb1f490
"
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=
"
25e934a301b56793018f8f5a6c1fcbb
0"
sum=
"
d0b7fd710c351e592979bcc9600518a
0"
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=
"
712a396952c0862e9b49f34fbb2490a4
"
sum=
"
67a9ee6bddfb767e24a859b7e4e2d73b
"
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=
"
848484923f90fda7b54b0309d43d9ed9
"
sum=
"
5a60893865bbd988e64a9272e32b1666
"
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=
"
85912351fe83419299848e3f5c1982cf
"
sum=
"
b1b296d0eb89514f1f4637ebbd9cdf54
"
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=
"
cc20ae36074a4fe51b188d4927f81fae
"
sum=
"
6b131cc2b0281f82b24ae6cdf7e4d642
"
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=
"
506cd4fc7abe3051f3451cd813ebd7e5
"
sum=
"
c315ed5d4f79c82fc33b2c637f5b4e82
"
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=
"9
2416b4cea2ff50735cc4e2e7ab09e11
"
sum=
"9
0ba9d96eb6af60a3f6141dde342b79f
"
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=
"
9914171d51b71c9ca355479fee156dd
f"
sum=
"
cf8c5ee59e56dd17d498b0004c75563
f"
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=
"
acc7d49d1d594b413ff8ad925ef65895
"
sum=
"
2ad89e9fa28d14d0e49491898a532347
"
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=
"
600958f14f18d4b436f4e24e405f4c0a
"
sum=
"
7fa3f41ceedf1ba887b9e62934dfec6b
"
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=
"
012d67bc12d6e7a273a74e9f2812db42
"
sum=
"
eac575e8935fe44ff4d4b17683334106
"
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=
"5
f601b642bda04bb8d27914557493751
"
sum=
"5
9137e0a4a9c5f4ca1afb4a1f0717aea
"
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=
"
cbe226da784c47693bb2e350a1bdde29
"
sum=
"
2a5375165ff9376cafe3549f557f138b
"
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=
"
113b98cf818e0719b63f98f415cdaf65
"
sum=
"
d9de67f80a13e750a37acb2eeb1e171a
"
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=
"
7186098d5475577625401728ddb97ad7
"
sum=
"
9b7735dc23b557512f8bdaf38093e098
"
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=
"
d931e1fc4b18ce57bbfd25c024d85e14
"
sum=
"
3a0d5bfdb6a61eb7142cca3997a77eec
"
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=
"
d7c3376ec359790570f411ad399a7c17
"
sum=
"
62871c0385134d7aad941b16dad9f749
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V2aminmaxV0V1Iiainfix <aminmaxV0V1ainfinityAainfix <aprefix -ainfinityaminmaxV0V1ainfix =V2aminmaxV0V1iainfix <=aminmaxV0V1aprefix -ainfinityainfix <=V2aprefix -ainfinityainfix >=V2ainfinityFAainfix >=V1c0Iainfix >=V1c0F"
>
...
...
examples/arm/why3session.xml
View file @
59cecc21
...
...
@@ -24,7 +24,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"VC for insertion_sort"
sum=
"
6152c465572f116cb4cbdb54cec6b773
"
sum=
"
1aa1097194b9d30e0d6cf83318c97522
"
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=
"
492d92d7d4a40e7717e9736c5599571
6"
sum=
"
be65e531a5cbe80f994990f8c4c9def
6"
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=
"
60875edac419a47f205013458f0c3aaa
"
sum=
"
bf489e6e0f7c734a74e018900e78e6a4
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V0c9Iainfix =V4aFalseIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F"
>
...
...
examples/assigning_meanings_to_programs/why3session.xml
View file @
59cecc21
...
...
@@ -24,7 +24,7 @@
locfile=
"../assigning_meanings_to_programs.mlw"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for sum"
sum=
"
e5449116862cde6a2205cd02a7dd9c87
"
sum=
"
17bf6dcb57a723007ce152bd4c333f35
"
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=
"
ccffd2d7ddad41347cee5271c0a9084a
"
sum=
"
352ca50c3d4c76f18b7506ce94f9c734
"
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 @
59cecc21
This diff is collapsed.
Click to expand it.
examples/binary_search/why3session.xml
View file @
59cecc21
...
...
@@ -24,7 +24,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"17"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"
bf18b515f2c894d5db932ad78fee5634
"
sum=
"
c86183765ebe55f456ec08cc12a1b26c
"
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=
"
879ca87287941f4aa56da3ad6004b34c
"
sum=
"
2ded482b93801cf9ecea5676d0a962b6
"
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=
"
125dc9e9bac17f79389aa05e99948642
"
sum=
"
b37d691aded290cf8f122f4c3f686b9b
"
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 @
59cecc21
...
...
@@ -24,7 +24,7 @@
locfile=
"../binary_sqrt.mlw"
loclnum=
"11"
loccnumb=
"10"
loccnume=
"14"
expl=
"VC for sqrt"
sum=
"
fbe8d4cdd0fda0789cc75fd2d45c4b8a
"
sum=
"
ec72b8f9dcaf436c3f1183ac92eb912e
"
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=
"
80f929942ef3003403011f6d530d8929
"
sum=
"
251e9c36cabe9e7b9541d0f06a00b8da
"
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=
"
0ef06faae32360da6c2c5b5b0ae7fc16
"
sum=
"
63b9ff6626db8664fff81a5f7ae74ffb
"
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=
"
e722c9edee4c20a09eaded8c428b3cb1
"
sum=
"
82efdbe2db3161daca3a638eb5423416
"
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/double/why3session.xml
View file @
59cecc21
...
...
@@ -50,7 +50,7 @@
name=
"nth_one1"
locfile=
"../double.why"
loclnum=
"73"
loccnumb=
"8"
loccnume=
"16"
sum=
"
d741dc4a8864da5f762e6b4c9e216431
"
sum=
"
779313c3d425e95c0f0b6bc0a29d053c
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =anthaoneV0aFalseIainfix <=V0c51Aainfix <=c0V0F"
>
...
...
@@ -75,7 +75,7 @@
name=
"nth_one2"
locfile=
"../double.why"
loclnum=
"74"
loccnumb=
"8"
loccnume=
"16"
sum=
"
82db89598d55d5fc2523ad127118d0f3
"
sum=
"
5477c865128db4a06170fe56521033ea
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =anthaoneV0aTrueIainfix <=V0c61Aainfix <=c52V0F"
>
...
...
@@ -93,14 +93,14 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
3
4"
/>
<result
status=
"valid"
time=
"0.4
8
"
/>
</proof>
</goal>
<goal
name=
"nth_one3"
locfile=
"../double.why"
loclnum=
"75"
loccnumb=
"8"
loccnume=
"16"
sum=
"4
5875e4d888b505655bcc262a708479b
"
sum=
"4
e7b6a6c83accd8455de3bcec4837f83
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =anthaoneV0aFalseIainfix <=V0c63Aainfix <=c62V0F"
>
...
...
@@ -117,7 +117,7 @@
name=
"sign_one"
locfile=
"../double.why"
loclnum=
"77"
loccnumb=
"8"
loccnume=
"16"
sum=
"
0e40a7449cdd9cd757fe90de1132610
0"
sum=
"
83d7589239f4c6d2e0b47583806bbcb
0"
proved=
"true"
expanded=
"false"
shape=
"ainfix =asignaoneaFalse"
>
...
...
@@ -166,7 +166,7 @@
name=
"exp_one"
locfile=
"../double.why"
loclnum=
"78"
loccnumb=
"8"
loccnume=
"15"
sum=
"
04f04c76f65ba3a4cd9f0dfb813700e8
"
sum=
"
13ba2625ca3b65718fabd943e1118361
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =aexpaonec1023"
>
...
...
@@ -192,7 +192,7 @@
name=
"mantissa_one"
locfile=
"../double.why"
loclnum=
"79"
loccnumb=
"8"
loccnume=
"20"
sum=
"
5565b958517fda2ea188aebd58fcbe3a
"
sum=
"
d68b4d3fc28fe2b05825830ca598d542
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =amantissaaonec0"
>
...
...
@@ -225,7 +225,7 @@
name=
"double_value_of_1"
locfile=
"../double.why"
loclnum=
"81"
loccnumb=
"8"
loccnume=
"25"
sum=
"
cfde4189a06549a716415b04a6741ede
"
sum=
"
ea478edc5021232fd4ec18211014adc7
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =adouble_of_bv64aonec1.0"
>
...
...
examples/bitvectors/neg_as_xor/why3session.xml
View file @
59cecc21
...
...
@@ -35,7 +35,7 @@
name=
"Nth_j"
locfile=
"../neg_as_xor.why"
loclnum=
"13"
loccnumb=
"8"
loccnume=
"13"
sum=
"
867cfc6f0844a2813914e1bb330e27d0
"
sum=
"
706d233bc684b53d77c1fdf517fed1a4
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =anthajV0aFalseIainfix <=V0c62Aainfix <=c0V0F"
>
...
...
@@ -53,14 +53,14 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"
0.83
"
/>
<result
status=
"valid"
time=
"
1.02
"
/>
</proof>
</goal>
<goal
name=
"sign_of_j"
locfile=
"../neg_as_xor.why"
loclnum=
"15"
loccnumb=
"8"
loccnume=
"17"
sum=
"
dd02f5f43382c4ceced221805af649dd
"
sum=
"
7b992f0a4a99d2dd8aae9c7d40278786
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =asignajaTrue"
>
...
...
@@ -77,7 +77,7 @@
name=
"mantissa_of_j"
locfile=
"../neg_as_xor.why"
loclnum=
"16"
loccnumb=
"8"
loccnume=
"21"
sum=
"
29f66aac078857c3b74a607f2009e1d7
"
sum=
"
8e1c2eee6de312bd6c82d7cbd1732b05
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =amantissaajc0"
>
...
...
@@ -103,14 +103,14 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"
2.68
"
/>
<result
status=
"valid"
time=
"
3.05
"
/>
</proof>
</goal>
<goal
name=
"exp_of_j"
locfile=
"../neg_as_xor.why"
loclnum=
"17"
loccnumb=
"8"
loccnume=
"16"
sum=
"
4bffb7900324096b7f864e9762cdde4d
"
sum=
"
372763ac7057bf0479a0525ae7232e67
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =aexpajc0"
>
...
...
@@ -143,7 +143,7 @@
name=
"int_of_bv"
locfile=
"../neg_as_xor.why"
loclnum=
"18"
loccnumb=
"8"
loccnume=
"17"
sum=
"47
516aa36e225dcd9557c2336828fe2e
"
sum=
"47
63b9cc56af1466f0d3108247919fd7
"