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
2508ec86
Commit
2508ec86
authored
Oct 06, 2012
by
Andrei Paskevich
Browse files
update sessions
parent
965cc977
Changes
33
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/foveoos2011/array_max/why3session.xml
View file @
2508ec86
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
users/demons/melquion/src/why3
/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
home/andrei/prj/why-git
/share/why3session.dtd">
<why3session
name=
"foveoos2011/array_max/why3session.xml"
shape_version=
"2"
>
<prover
...
...
@@ -29,7 +29,7 @@
locfile=
"foveoos2011/array_max/../array_max.mlw"
loclnum=
"21"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter max"
sum=
"
c17ee58010c97dbec6b35d25af7878b
9"
sum=
"
e8de669fdf43b35dd32e52ba558b85d
9"
proved=
"true"
expanded=
"true"
shape=
"iainfix =V3V2Niainfix <=agetV1V3agetV1V2ainfix <ainfix -V2V4ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix <=agetV1V5amaxagetV1V4agetV1V2Iainfix <V5V0Aainfix <V2V5Oainfix <V5V4Aainfix <=c0V5FAainfix <V2V0Aainfix <=V4V2Aainfix <=c0V4Iainfix =V4ainfix +V3c1Fainfix <ainfix -V6V3ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix <=agetV1V7amaxagetV1V3agetV1V6Iainfix <V7V0Aainfix <V6V7Oainfix <V7V3Aainfix <=c0V7FAainfix <V6V0Aainfix <=V3V6Aainfix <=c0V3Iainfix =V6ainfix -V2c1FAainfix <V3V0Aainfix <=c0V3Aainfix <V2V0Aainfix <=c0V2ainfix <=agetV1V8agetV1V3Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V3Iainfix <=agetV1V9amaxagetV1V3agetV1V2Iainfix <V9V0Aainfix <V2V9Oainfix <V9V3Aainfix <=c0V9FAainfix <V2V0Aainfix <=V3V2Aainfix <=c0V3FAainfix <=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix <V10V0Aainfix <ainfix -V0c1V10Oainfix <V10c0Aainfix <=c0V10FAainfix <ainfix -V0c1V0Aainfix <=c0ainfix -V0c1Aainfix <=c0c0Iainfix <c0V0FF"
>
...
...
@@ -41,7 +41,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
<proof
prover=
"1"
...
...
@@ -57,7 +57,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"2.3
8
"
/>
<result
status=
"valid"
time=
"2.3
4
"
/>
</proof>
</goal>
</theory>
...
...
examples/foveoos2011/duplets/why3session.xml
View file @
2508ec86
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
users/demons/melquion/src/why3
/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
home/andrei/prj/why-git
/share/why3session.dtd">
<why3session
name=
"foveoos2011/duplets/why3session.xml"
shape_version=
"2"
>
<prover
...
...
@@ -36,7 +36,7 @@
locfile=
"foveoos2011/duplets/../duplets.mlw"
loclnum=
"43"
loccnumb=
"6"
loccnume=
"12"
expl=
"parameter duplet"
sum=
"
c4ca31cc7efa0d509fd5d930d7d0daef
"
sum=
"
18fdae12af8c0e3d1e3cb70ddbf7f8f8
"
proved=
"true"
expanded=
"true"
shape=
"ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix <V5V0Aainfix <V4V5Aainfix <V4ainfix +ainfix -V0c2c1Aainfix <=c0V4FNAiCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix <V11V0Aainfix <V10V11Aainfix <V10ainfix +V7c1Aainfix <=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix <V14V0Aainfix <V13V14Aainfix <V13ainfix +V7c1Aainfix <=c0V13FIais_dupletV3V7V16NIainfix <V16ainfix +ainfix -V0c1c1Aainfix <V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =V19V17Aainfix =V18V7Fais_dupletV3V7V21NIainfix <V21ainfix +V17c1Aainfix <V7V21FAainfix <V17V0Aainfix <=c0V17Iais_dupletV3V7V22NIainfix <V22V17Aainfix <V7V22FIainfix <=V17ainfix -V0c1Aainfix <=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix <V23ainfix +V7c1Aainfix <V7V23FIainfix <=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix <V25V0Aainfix <V24V25Aainfix <V24ainfix +V7c1Aainfix <=c0V24FIainfix >ainfix +V7c1ainfix -V0c1LagetV2V7Aainfix <V7V0Aainfix <=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix <V28V0Aainfix <V27V28Aainfix <V27V7Aainfix <=c0V27FIainfix <=V7ainfix -V0c2Aainfix <=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix <V31V0Aainfix <V30V31Aainfix <V30c0Aainfix <=c0V30FIainfix <=c0ainfix -V0c2Aainfix >c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix <=c2V0Lamk arrayV0V2FF"
>
...
...
@@ -64,7 +64,7 @@
locfile=
"foveoos2011/duplets/../duplets.mlw"
loclnum=
"75"
loccnumb=
"6"
loccnume=
"13"
expl=
"parameter duplets"
sum=
"
3c9ebe0a2cfbf042bd5817d47b00ced
f"
sum=
"
e99b05c40c9b643592e49bc2013aff3
f"
proved=
"true"
expanded=
"true"
shape=
"ainfix =agetV1V3agetV1V6NAais_dupletV2V6V7Aais_dupletV2V3V4Iainfix =V5agetV1V6NAais_dupletV2V6V7FAainfix =V5agetV1V8NAais_dupletV2V8V9EAainfix <=c2V0LagetV1V4Aainfix <V4V0Aainfix <=c0V4Iais_dupletV2V3V4FAais_dupletV2V10V11EAainfix <=c2V0Iainfix =agetV1V12agetV1V14NAais_dupletV2V14V15Aais_dupletV2V12V13EAainfix <=c4V0Lamk arrayV0V1FF"
>
...
...
@@ -76,7 +76,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
4
"
/>
</proof>
<proof
prover=
"1"
...
...
@@ -84,7 +84,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -92,7 +92,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
</theory>
...
...
examples/programs/algo63/why3session.xml
View file @
2508ec86
This diff is collapsed.
Click to expand it.
examples/programs/algo64/why3session.xml
View file @
2508ec86
...
...
@@ -25,7 +25,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"parameter quicksort"
sum=
"8
90b7e54699a43c7807902174a13a41e
"
sum=
"8
ce983870add1b671d5acb4720e907c7
"
proved=
"true"
expanded=
"true"
shape=
"iainfix <V1V2asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Aapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FAainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Aainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Aapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FAainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Aainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FAainfix <V2V0Aainfix <V1V2Aainfix <=c0V1asorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -40,7 +40,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"precondition"
sum=
"
3e511163b0114754c42c48becabb9109
"
sum=
"
98154b0bb9e9cf79f5701a8c8d9f8862
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -59,8 +59,8 @@
name=
"WP_parameter quicksort.2"
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"variant decrease
s
"
sum=
"
b6bdb89212e2a15a9898dc6215e84df7
"
expl=
"variant decrease"
sum=
"
c6fce40c4d56cf1d86ea343cc8663826
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -72,7 +72,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -80,7 +80,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"precondition"
sum=
"
556516d8bd4549b79a2d6b5e7d46628a
"
sum=
"
6699bdb6c0edbf732892993ca660692d
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -92,7 +92,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -100,7 +100,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"assertion"
sum=
"
e38f0c946373a1995809ee5c0c466dfe
"
sum=
"
447aca98da7fe7db957540e379d4b2d5
"
proved=
"true"
expanded=
"false"
shape=
"apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -112,15 +112,15 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter quicksort.5"
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"variant decrease
s
"
sum=
"
1db9ef0fd17e657063f61aac9148fd8d
"
expl=
"variant decrease"
sum=
"
5f75860636670ea0b4d0d4125390adac
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -140,7 +140,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"precondition"
sum=
"
3230e43afcedfba2f5761b2bd5dd4b93
"
sum=
"
79be74f3588ada732be11fa60093db5f
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -152,7 +152,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -160,7 +160,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"assertion"
sum=
"
af85ec1817492490de4d45b7179a286
6"
sum=
"
9dac3b3ed92a3afc6800798ded2ac4d
6"
proved=
"true"
expanded=
"false"
shape=
"apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -179,8 +179,8 @@
name=
"WP_parameter quicksort.8"
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"
normal
postcondition"
sum=
"
fb860a740a4ce478030b7ab12d6a50d3
"
expl=
"postcondition"
sum=
"
c867d711c1258570114f0d162574c767
"
proved=
"true"
expanded=
"true"
shape=
"asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -195,7 +195,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"parameter quicksort"
sum=
"
4b8b04d1cf923b7889d14fdb2530f478
"
sum=
"
13b1e0f734ce07d1a81bcdd3442aebe7
"
proved=
"true"
expanded=
"false"
shape=
"apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -215,7 +215,7 @@
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"parameter quicksort"
sum=
"
ffb31b94e3cf8ede84148c2b2743d6a8
"
sum=
"
64700d77b60a90271005c75455b8e88e
"
proved=
"true"
expanded=
"true"
shape=
"asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
@@ -223,11 +223,11 @@
name=
"expl:parameter quicksort"
/>
<proof
prover=
"1"
timelimit=
"3
0
"
timelimit=
"3
6
"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"
17.93
"
/>
<result
status=
"valid"
time=
"
4.14
"
/>
</proof>
</goal>
</transf>
...
...
@@ -236,8 +236,8 @@
name=
"WP_parameter quicksort.9"
locfile=
"programs/algo64/../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"
normal
postcondition"
sum=
"
f14de86a78b3bf6015f0f66c618648f4
"
expl=
"postcondition"
sum=
"
8ccaf2253bd77eeaea8070a64dad234a
"
proved=
"true"
expanded=
"false"
shape=
"asorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1FF"
>
...
...
examples/programs/algo65/why3session.xml
View file @
2508ec86
This diff is collapsed.
Click to expand it.
examples/programs/arm/why3session.xml
View file @
2508ec86
...
...
@@ -25,7 +25,7 @@
locfile=
"examples/programs/arm/../arm.mlw"
loclnum=
"17"
loccnumb=
"6"
loccnume=
"20"
expl=
"parameter insertion_sort"
sum=
"
dbb9dfe3f395d80dedbd7726d136285d
"
sum=
"
7748fd507776784f81c6745ae3a11c7f
"
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 -V11c1agetV13V11FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1FAainfix <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 -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Lamk arrayV0V3FF"
>
...
...
@@ -50,7 +50,7 @@
name=
"WP_parameter path_init_l2"
locfile=
"examples/programs/arm/../arm.mlw"
loclnum=
"122"
loccnumb=
"6"
loccnume=
"18"
expl=
"
normal
postcondition"
expl=
"postcondition"
sum=
"795f8de35a06a3c2af46ce51dec5f462"
proved=
"true"
expanded=
"true"
...
...
@@ -63,7 +63,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.0
1
"
/>
<result
status=
"unknown"
time=
"0.0
2
"
/>
</proof>
<proof
prover=
"1"
...
...
@@ -78,7 +78,7 @@
name=
"WP_parameter path_l2_exit"
locfile=
"examples/programs/arm/../arm.mlw"
loclnum=
"129"
loccnumb=
"6"
loccnume=
"18"
expl=
"
normal
postcondition"
expl=
"postcondition"
sum=
"15ab5996d34e86896c649b5e2e7646ff"
proved=
"true"
expanded=
"true"
...
...
@@ -91,7 +91,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
</theory>
...
...
examples/programs/assigning_meanings_to_programs/why3session.xml
View file @
2508ec86
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
users/demons/melquion/src/why3
/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
home/andrei/prj/why-git
/share/why3session.dtd">
<why3session
name=
"programs/assigning_meanings_to_programs/why3session.xml"
shape_version=
"2"
>
<prover
...
...
@@ -25,7 +25,7 @@
locfile=
"programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter sum"
sum=
"
cf5b6add86b933c98cd7dd609a2b18ba
"
sum=
"
00e2802392a17c1b774dc7fe33cef4a1
"
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 <=c0V1FF"
>
...
...
examples/programs/binary_search/why3session.xml
View file @
2508ec86
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
users/demons/melquion/src/why3
/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
home/andrei/prj/why-git
/share/why3session.dtd">
<why3session
name=
"programs/binary_search/why3session.xml"
shape_version=
"2"
>
<prover
...
...
@@ -25,7 +25,7 @@
locfile=
"programs/binary_search/../binary_search.mlw"
loclnum=
"17"
loccnumb=
"6"
loccnume=
"19"
expl=
"parameter binary_search"
sum=
"
e07fe8808065c91ab2d13bb09be220e1
"
sum=
"
9f60cf065e425aed250128303946138f
"
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 <=c0V12FFF"
>
...
...
@@ -45,7 +45,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
3
"
/>
</proof>
</goal>
</theory>
...
...
@@ -60,7 +60,7 @@
locfile=
"programs/binary_search/../binary_search.mlw"
loclnum=
"59"
loccnumb=
"6"
loccnume=
"19"
expl=
"parameter binary_search"
sum=
"
4d55592122a1fea6cf79c85bad7f1391
"
sum=
"
16ce454ae5e4d3346ff4a9dd4f84fba0
"
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 <=c0V13FFF"
>
...
...
@@ -87,7 +87,7 @@
locfile=
"programs/binary_search/../binary_search.mlw"
loclnum=
"99"
loccnumb=
"6"
loccnume=
"19"
expl=
"parameter binary_search"
sum=
"
33ef8438dfc4b808a3c8569c997cb51c
"
sum=
"
5f760c6ff02952c3cb4e9c6699b517ad
"
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/programs/checking_a_large_routine/why3session.xml
View file @
2508ec86
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
users/demons/melquion/src/why3
/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
home/andrei/prj/why-git
/share/why3session.dtd">
<why3session
name=
"programs/checking_a_large_routine/why3session.xml"
shape_version=
"2"
>
name=
"
examples/
programs/checking_a_large_routine/why3session.xml"
shape_version=
"2"
>
<prover
id=
"0"
name=
"Alt-Ergo"
...
...
@@ -13,16 +13,16 @@
<file
name=
"../checking_a_large_routine.mlw"
verified=
"true"
expanded=
"
fals
e"
>
expanded=
"
tru
e"
>
<theory
name=
"CheckingALargeRoutine"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"7"
loccnumb=
"7"
loccnume=
"28"
verified=
"true"
expanded=
"true"
>
<goal
name=
"WP_parameter routine"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"parameter routine"
sum=
"2c87a5e73941cd3b02af61bf8fce44e6"
...
...
@@ -37,7 +37,7 @@
expanded=
"true"
>
<goal
name=
"WP_parameter routine.1"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"loop invariant init"
sum=
"1f1332adbddf942e33b91fc159bd1721"
...
...
@@ -57,7 +57,7 @@
</goal>
<goal
name=
"WP_parameter routine.2"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"loop invariant init"
sum=
"3c949a8367aa36916278f22d2233e42b"
...
...
@@ -77,7 +77,7 @@
</goal>
<goal
name=
"WP_parameter routine.3"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"loop invariant preservation"
sum=
"16adecdb605315af127fab31763c4f24"
...
...
@@ -97,9 +97,9 @@
</goal>
<goal
name=
"WP_parameter routine.4"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"loop variant decrease
s
"
expl=
"loop variant decrease"
sum=
"658ecffa25b241aba563b686c7a7880d"
proved=
"true"
expanded=
"true"
...
...
@@ -117,7 +117,7 @@
</goal>
<goal
name=
"WP_parameter routine.5"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"loop invariant preservation"
sum=
"78ac374bb40b2a7ba345a472c13cbf81"
...
...
@@ -137,9 +137,9 @@
</goal>
<goal
name=
"WP_parameter routine.6"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"loop variant decrease
s
"
expl=
"loop variant decrease"
sum=
"cfe6e6f973867f21832faea47e50402e"
proved=
"true"
expanded=
"true"
...
...
@@ -157,9 +157,9 @@
</goal>
<goal
name=
"WP_parameter routine.7"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"13"
loccnumb=
"6"
loccnume=
"13"
expl=
"
normal
postcondition"
expl=
"postcondition"
sum=
"eb589caeed04d036cf730be9c7c45e0f"
proved=
"true"
expanded=
"true"
...
...
@@ -179,7 +179,7 @@
</goal>
<goal
name=
"WP_parameter routine2"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"parameter routine2"
sum=
"3a19abec2be89a45778d01d35bc323c6"
...
...
@@ -194,9 +194,9 @@
expanded=
"true"
>
<goal
name=
"WP_parameter routine2.1"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"
normal
postcondition"
expl=
"postcondition"
sum=
"704ab83d1cf9f3cc9a75b6d5dff22493"
proved=
"true"
expanded=
"true"
...
...
@@ -214,9 +214,9 @@
</goal>
<goal
name=
"WP_parameter routine2.2"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"
for
loop in
itialization
"
expl=
"loop in
variant init
"
sum=
"6f4355c291edd1a40e47bdd2b472aeee"
proved=
"true"
expanded=
"true"
...
...
@@ -234,13 +234,73 @@
</goal>
<goal
name=
"WP_parameter routine2.3"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
locfile=
"examples/programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"loop invariant preservation"
sum=
"9ff28d6d6d727b7dae866368db832070"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
<label
name=
"expl:parameter routine2"
/>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter routine2.4"
locfile=
"examples/programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"
for
loop
preservation
"
sum=
"
8417f7ee6b9b182f934023e1e05a8472
"
expl=
"loop
invariant init
"
sum=
"
cd8123d3adfacc7366bbe70963b4be4b
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
shape=
"ainfix =V1ainfix *c1afactV2Iainfix <=c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
<label
name=
"expl:parameter routine2"
/>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter routine2.5"
locfile=
"examples/programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"loop invariant preservation"
sum=
"a7a95f15d6b3c0699a8c1e9c9aad724c"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFIainfix <=c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
<label
name=
"expl:parameter routine2"
/>
<proof
prover=
"0"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter routine2.6"
locfile=
"examples/programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"loop invariant preservation"
sum=
"47be5d244ba8f38f45fa3321641b30e3"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2FIainfix <=c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"
>
<label
name=
"expl:parameter routine2"
/>
<proof
...
...
@@ -249,14 +309,14 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter routine2.
4
"
locfile=
"programs/checking_a_large_routine/../checking_a_large_routine.mlw"
name=
"WP_parameter routine2.
7
"
locfile=
"
examples/
programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum=
"34"
loccnumb=
"6"
loccnume=
"14"
expl=
"
normal
postcondition"
expl=
"postcondition"
sum=
"e8ed7c7dd8be78212fb8330764a50027"
proved=
"true"
expanded=
"true"
...
...
examples/programs/counting_sort/why3session.xml
View file @
2508ec86
This diff is collapsed.
Click to expand it.
examples/programs/decrease1/why3session.xml
View file @
2508ec86
This diff is collapsed.
Click to expand it.
examples/programs/fill/why3session.xml
View file @
2508ec86
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
users/demons/melquion/src/why3
/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
home/andrei/prj/why-git
/share/why3session.dtd">
<why3session
name=
"programs/fill/why3session.xml"
shape_version=
"2"
>
<prover
...
...
@@ -24,7 +24,7 @@
name=
"size_nonneg"
locfile=
"programs/fill/../fill.mlw"
loclnum=
"23"
loccnumb=
"8"
loccnume=
"19"
sum=
"
5a24afab440aa4447237e354a9ba830d
"
sum=
"
15fb75b07c7dc8b33727fc5bb880116a
"
proved=
"true"
expanded=
"true"
shape=
"ainfix >=asizeV0c0F"
>
...
...
@@ -35,15 +35,15 @@
edited=
"fill_WP_Fill_size_nonneg_2.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
52
"
/>
<result
status=
"valid"
time=
"0.
46
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter fill"
locfile=
"programs/fill/../fill.mlw"
loclnum=
"25"
loccnumb=
"10"
loccnume=
"14"
expl=
"p
arameter fill
"
sum=
"
2b575987987cb7e23acc0ad58dc38958
"
expl=
"p
ostcondition
"
sum=
"
4235fe223126421752857d12549df16f
"
proved=
"true"
expanded=
"true"
shape=
"CV0aNullacontainsV0agetV3V4Iainfix <V4V2Aainfix <=V2V4FAainfix =agetV3V5agetV3V5Iainfix <V5V2Aainfix <=c0V5FAainfix <=V2V1Aainfix <=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix <V14V13Aainfix <=V2V14FAainfix =agetV12V15agetV3V15Iainfix <V15V2Aainfix <=c0V15FAainfix <=V13V1Aainfix <=V2V13IacontainsV8agetV12V16Iainfix <V16V13Aainfix <=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix <V17ainfix +V10c1Aainfix <=c0V17FAainfix <=V13V1Aainfix <=ainfix +V10c1V13FFAainfix <=ainfix +V10c1V1Aainfix <=c0ainfix +V10c1Aainfix <asizeV8asizeV0Aainfix <=c0asizeV0Iainfix =V11asetV9V10V7FAainfix <V10V1Aainfix <=c0V10acontainsV0agetV9V18Iainfix <V18V10Aainfix <=V2V18FAainfix =agetV9V19agetV3V19Iainfix <V19V2Aainfix <=c0V19FAainfix <=V10V1Aainfix <=V2V10IacontainsV6agetV9V20Iainfix <V20V10Aainfix <=V2V20FAainfix =agetV9V21agetV3V21Iainfix <V21V2Aainfix <=c0V21FAainfix <=V10V1Aainfix <=V2V10FFAainfix <=V2V1Aainfix <=c0V2Aainfix <asizeV6asizeV0Aainfix <=c0asizeV0Iainfix <=V2V1Aainfix <=c0V2FF"
>
...
...
@@ -55,7 +55,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
7
"
/>
<result
status=
"valid"
time=
"0.0
6
"
/>