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
d3dfe8ec
Commit
d3dfe8ec
authored
Jun 28, 2014
by
MARCHE Claude
Browse files
compressed sessions
parent
2ce79f5a
Changes
456
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/add_list/why3session.xml
View file @
d3dfe8ec
...
...
@@ -2,66 +2,32 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"1"
name=
"Alt-Ergo"
version=
"0.95.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../add_list.mlw"
expanded=
"true"
>
<theory
name=
"SumList"
>
</theory>
<theory
name=
"AddListRec"
expanded=
"true"
>
<goal
name=
"WP_parameter sum"
expl=
"VC for sum"
sum=
"0ad629c2956d434cdf621a03e0b7c7ba"
expanded=
"true"
>
<label
name=
"expl:VC for sum"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"1"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"2"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter main"
expl=
"VC for main"
sum=
"6b4e350cd7d1b4015bab61dc01e96aec"
expanded=
"true"
>
<label
name=
"expl:VC for main"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"2"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
</theory>
<theory
name=
"AddListImp"
expanded=
"true"
>
<goal
name=
"WP_parameter sum"
expl=
"VC for sum"
sum=
"82f58e47d4e58d15d59a87efee2a6ad8"
expanded=
"true"
>
<label
name=
"expl:VC for sum"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"2"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter main"
expl=
"VC for main"
sum=
"9051692e9ac1a4d1f56386a0fd7d440f"
expanded=
"true"
>
<label
name=
"expl:VC for main"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"2"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
</theory>
</file>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.95.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"1"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../add_list.mlw"
expanded=
"true"
>
<theory
name=
"SumList"
>
</theory>
<theory
name=
"AddListRec"
expanded=
"true"
>
<goal
name=
"WP_parameter sum"
expl=
"VC for sum"
sum=
"0ad629c2956d434cdf621a03e0b7c7ba"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter main"
expl=
"VC for main"
sum=
"6b4e350cd7d1b4015bab61dc01e96aec"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</theory>
<theory
name=
"AddListImp"
expanded=
"true"
>
<goal
name=
"WP_parameter sum"
expl=
"VC for sum"
sum=
"82f58e47d4e58d15d59a87efee2a6ad8"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter main"
expl=
"VC for main"
sum=
"9051692e9ac1a4d1f56386a0fd7d440f"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</theory>
</file>
</why3session>
examples/add_list/why3shapes.dat
deleted
100644 → 0
View file @
2ce79f5a
0ad629c2956d434cdf621a03e0b7c7ba Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F
6b4e350cd7d1b4015bab61dc01e96aec ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil
82f58e47d4e58d15d59a87efee2a6ad8 ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F
9051692e9ac1a4d1f56386a0fd7d440f ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil
examples/add_list/why3shapes.gz
0 → 100644
View file @
d3dfe8ec
File added
examples/algo63/why3session.xml
View file @
d3dfe8ec
This diff is collapsed.
Click to expand it.
examples/algo63/why3shapes.dat
deleted
100644 → 0
View file @
2ce79f5a
This diff is collapsed.
Click to expand it.
examples/algo63/why3shapes.gz
0 → 100644
View file @
d3dfe8ec
File added
examples/algo64/why3session.xml
View file @
d3dfe8ec
...
...
@@ -2,139 +2,65 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../algo64.mlw"
expanded=
"true"
>
<theory
name=
"Algo64"
expanded=
"true"
>
<goal
name=
"WP_parameter quicksort"
expl=
"VC for quicksort"
sum=
"b3c80285a2f93720ffbeec07fe9484f7"
expanded=
"true"
>
<label
name=
"expl:VC for quicksort"
/>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter quicksort.1"
expl=
"1. precondition"
sum=
"60641f0dd6fd791e2eb04365466e4b67"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.2"
expl=
"2. variant decrease"
sum=
"d044cdfb327536252d9d35d6c8c8d779"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.3"
expl=
"3. precondition"
sum=
"c51bbed49cb41b5186ee449ca22b5d0f"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.4"
expl=
"4. assertion"
sum=
"a62cc8ba874159b234bb59428fe08b3c"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.14"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.5"
expl=
"5. variant decrease"
sum=
"cbc7bedb98f7451986a3718eda496a7c"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.6"
expl=
"6. precondition"
sum=
"fff053c1414e1610d034118e841c6500"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.7"
expl=
"7. assertion"
sum=
"c286faac90136a80939022ab618896af"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"2.07"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.8"
expl=
"8. postcondition"
sum=
"bf52bb94f3ce94cc8aeb29cfbd99aba5"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.53"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.9"
expl=
"9. postcondition"
sum=
"97cc3e363dcba7833cc03add00eca267"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.16"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.10"
expl=
"10. postcondition"
sum=
"16dcef28364b3606b5af7ea67b96d36c"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.11"
expl=
"11. postcondition"
sum=
"a2af1e38ef1266733de9df088d4b57d3"
>
<label
name=
"expl:VC for quicksort"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter qs"
expl=
"VC for qs"
sum=
"c020ba36a9f1cbc706a81299d7e67dc5"
>
<label
name=
"expl:VC for qs"
/>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter qs.1"
expl=
"1. precondition"
sum=
"af20b26413ca9ad74cd53bb91ad9bf58"
>
<label
name=
"expl:VC for qs"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter qs.2"
expl=
"2. postcondition"
sum=
"8c72e4401654ed269af73c95614802d2"
>
<label
name=
"expl:VC for qs"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter qs.3"
expl=
"3. postcondition"
sum=
"abf810b8c32150c26b4a3f3e6aacac6e"
>
<label
name=
"expl:VC for qs"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter qs.4"
expl=
"4. postcondition"
sum=
"ba4a3b43dca6859d783d70d4c5b16669"
>
<label
name=
"expl:VC for qs"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter qs.5"
expl=
"5. postcondition"
sum=
"8532155787a9b770710dad8ca4324c1f"
>
<label
name=
"expl:VC for qs"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../algo64.mlw"
expanded=
"true"
>
<theory
name=
"Algo64"
expanded=
"true"
>
<goal
name=
"WP_parameter quicksort"
expl=
"VC for quicksort"
sum=
"b3c80285a2f93720ffbeec07fe9484f7"
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter quicksort.1"
expl=
"1. precondition"
sum=
"60641f0dd6fd791e2eb04365466e4b67"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.2"
expl=
"2. variant decrease"
sum=
"d044cdfb327536252d9d35d6c8c8d779"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.3"
expl=
"3. precondition"
sum=
"c51bbed49cb41b5186ee449ca22b5d0f"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.4"
expl=
"4. assertion"
sum=
"a62cc8ba874159b234bb59428fe08b3c"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.14"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.5"
expl=
"5. variant decrease"
sum=
"cbc7bedb98f7451986a3718eda496a7c"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.6"
expl=
"6. precondition"
sum=
"fff053c1414e1610d034118e841c6500"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.7"
expl=
"7. assertion"
sum=
"c286faac90136a80939022ab618896af"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"2.07"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.8"
expl=
"8. postcondition"
sum=
"bf52bb94f3ce94cc8aeb29cfbd99aba5"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.53"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.9"
expl=
"9. postcondition"
sum=
"97cc3e363dcba7833cc03add00eca267"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.16"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.10"
expl=
"10. postcondition"
sum=
"16dcef28364b3606b5af7ea67b96d36c"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter quicksort.11"
expl=
"11. postcondition"
sum=
"a2af1e38ef1266733de9df088d4b57d3"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter qs"
expl=
"VC for qs"
sum=
"c020ba36a9f1cbc706a81299d7e67dc5"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter qs.1"
expl=
"1. precondition"
sum=
"af20b26413ca9ad74cd53bb91ad9bf58"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter qs.2"
expl=
"2. postcondition"
sum=
"8c72e4401654ed269af73c95614802d2"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter qs.3"
expl=
"3. postcondition"
sum=
"abf810b8c32150c26b4a3f3e6aacac6e"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter qs.4"
expl=
"4. postcondition"
sum=
"ba4a3b43dca6859d783d70d4c5b16669"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter qs.5"
expl=
"5. postcondition"
sum=
"8532155787a9b770710dad8ca4324c1f"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/algo64/why3shapes.dat
deleted
100644 → 0
View file @
2ce79f5a
b3c80285a2f93720ffbeec07fe9484f7 iasorted_subV1V2ainfix +V3c1Aapermut_subV4V4V2ainfix +V3c1asorted_subV11V2ainfix +V3c1Aapermut_subV4V12V2ainfix +V3c1Aaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FAainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Aaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FAainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Aainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FAainfix <V3V0Aainfix <V2V3Aainfix <=c0V2ainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
60641f0dd6fd791e2eb04365466e4b67 preconditionainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
d044cdfb327536252d9d35d6c8c8d779 variant decreaseainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
c51bbed49cb41b5186ee449ca22b5d0f preconditionainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
a62cc8ba874159b234bb59428fe08b3c assertionaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
cbc7bedb98f7451986a3718eda496a7c variant decreaseainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
fff053c1414e1610d034118e841c6500 preconditionainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
c286faac90136a80939022ab618896af assertionaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
bf52bb94f3ce94cc8aeb29cfbd99aba5 postconditionapermut_subV4V12V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
97cc3e363dcba7833cc03add00eca267 postconditionasorted_subV11V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
16dcef28364b3606b5af7ea67b96d36c postconditionapermut_subV4V4V2ainfix +V3c1INainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
a2af1e38ef1266733de9df088d4b57d3 postconditionasorted_subV1V2ainfix +V3c1INainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
c020ba36a9f1cbc706a81299d7e67dc5 iasorted_subV1c0V0Aapermut_allV2V2asorted_subV4c0V0Aapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FAainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1ainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
af20b26413ca9ad74cd53bb91ad9bf58 preconditionainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
8c72e4401654ed269af73c95614802d2 postconditionapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FIainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
abf810b8c32150c26b4a3f3e6aacac6e postconditionasorted_subV4c0V0Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FIainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
ba4a3b43dca6859d783d70d4c5b16669 postconditionapermut_allV2V2INainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
8532155787a9b770710dad8ca4324c1f postconditionasorted_subV1c0V0INainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
examples/algo64/why3shapes.gz
0 → 100644
View file @
d3dfe8ec
File added
examples/algo65/why3session.xml
View file @
d3dfe8ec
...
...
@@ -2,311 +2,138 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../algo65.mlw"
expanded=
"true"
>
<theory
name=
"Algo65"
expanded=
"true"
>
<goal
name=
"WP_parameter find"
expl=
"VC for find"
sum=
"6868a7addea3afd6aefa8d9aa500c4dc"
expanded=
"true"
>
<label
name=
"expl:VC for find"
/>
<transf
name=
"split_goal"
expanded=
"true"
>
<goal
name=
"WP_parameter find.1"
expl=
"1. precondition"
sum=
"cf061e6b0c714b137f5b85834f75c045"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.00"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.2"
expl=
"2. variant decrease"
sum=
"a220fe990bf8270627c276501ad45e38"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.00"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.3"
expl=
"3. precondition"
sum=
"82a3df1ed87ce5e4bb60696b5f6a3825"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.4"
expl=
"4. assertion"
sum=
"fca08a55f93b232b4ad0c12ac4cbe9ce"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.5"
expl=
"5. assertion"
sum=
"611a958d5fef40cbafefc98b75bffa4d"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.6"
expl=
"6. assertion"
sum=
"ed9124e274593de98fac324c81bf7245"
expanded=
"true"
>
<label
name=
"expl:VC for find"
/>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter find.6.1"
expl=
"1. assertion"
sum=
"3146622a4f15a5bf2b8b9cb7bf70dd43"
expanded=
"true"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
timelimit=
"6"
>
<result
status=
"valid"
time=
"0.19"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.6.2"
expl=
"2. assertion"
sum=
"e7631e9a86bd4136b65da1d42a82c807"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.11"
/>
</proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter find.7"
expl=
"7. variant decrease"
sum=
"d6f051702eae57638697208968e570d5"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.8"
expl=
"8. precondition"
sum=
"a81e1cb1c269da1f11dab3955f3b9f53"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.9"
expl=
"9. assertion"
sum=
"050916e733a8abc8f1240832dc4f8743"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.10"
expl=
"10. assertion"
sum=
"b7afc00bc364084b94495440f0c56cd7"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.11"
expl=
"11. assertion"
sum=
"b3b44a7e1c5e0e4d9cbd64f68acee82b"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.12"
expl=
"12. postcondition"
sum=
"bb5774bdeb0f6de6e33539d629f1fc47"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.13"
expl=
"13. postcondition"
sum=
"ace58a0a0af2452f20ba3cc6bee7a1ff"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.14"
expl=
"14. postcondition"
sum=
"d4274f39a4d9a3988b0a9350791059c7"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.15"
expl=
"15. assertion"
sum=
"23c7795c72accf45e816adc86111d0e6"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.16"
expl=
"16. assertion"
sum=
"46601176c8bce521c2b5e8b3cdef9e46"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.38"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.17"
expl=
"17. postcondition"
sum=
"5ca076829a6dca77ec3295edbc24e302"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.18"
expl=
"18. postcondition"
sum=
"7ae7e503d1f1c56492aadee5e6c148a5"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.19"
expl=
"19. postcondition"
sum=
"d699c7c1c0240e53b960aea5b968334c"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.31"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.20"
expl=
"20. assertion"
sum=
"d51d465d2733ba90f6a8cd9b0d4188d5"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.21"
expl=
"21. assertion"
sum=
"3bd11013b6347e5b0ce603840d0e61a8"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.22"
expl=
"22. variant decrease"
sum=
"60dc3bbdbbe8c13cd4a598f9ca7970e1"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.23"
expl=
"23. precondition"
sum=
"3e017f8cc37735ada2c643ca0277fd48"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.24"
expl=
"24. assertion"
sum=
"7273309b4f11ac8b28fe9cf94cc0d5e9"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.25"
expl=
"25. assertion"
sum=
"e5450e1070053b8b21b5524adc818bc5"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.26"
expl=
"26. assertion"
sum=
"66a97e2afd938ff54fa2e76e2e63d72e"
expanded=
"true"
>
<label
name=
"expl:VC for find"
/>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter find.26.1"
expl=
"1. assertion"
sum=
"17565d374941f5cd2fdfc12fd5b46a2e"
expanded=
"true"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
timelimit=
"6"
>
<result
status=
"valid"
time=
"0.24"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.26.2"
expl=
"2. assertion"
sum=
"b8157af81a7f2cea28ee5eba0529e815"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.25"
/>
</proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter find.27"
expl=
"27. postcondition"
sum=
"4be978c8aa81e1e8d04f01cf77aec93e"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.28"
expl=
"28. postcondition"
sum=
"594f0e3452dfe9da6eb6b5c601022102"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.32"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.29"
expl=
"29. postcondition"
sum=
"81c6d96a20e09585b55e8209e4a60b6c"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.30"
expl=
"30. assertion"
sum=
"a2c453f787c7d4ad06b1832977ba6964"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.31"
expl=
"31. assertion"
sum=
"22301f65968a1948d798fb8f406315f8"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.32"
expl=
"32. postcondition"
sum=
"28eb85680f8896c3847e6248c8cff17f"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter find.33"
expl=
"33. postcondition"
sum=
"e399b60fde9a3c31959fdc79f480442f"
>
<label
name=
"expl:VC for find"
/>
<proof
prover=
"0"
>