Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
b4a01678
Commit
b4a01678
authored
May 24, 2012
by
MARCHE Claude
Browse files
UPdated sessions after addition of lemmas on division
parent
a7d6c9ad
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/check-builtin/euclideandivision/why3session.xml
View file @
b4a01678
...
...
@@ -32,7 +32,7 @@
name=
"G1"
locfile=
"check-builtin/euclideandivision/../euclideandivision.why"
loclnum=
"3"
loccnumb=
"12"
loccnume=
"14"
sum=
"
c9dce8acf8d17f8bb9290708121a5df2
"
sum=
"
73c47861b347211a7dc97e723e8ebc83
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =amodc10c3c1"
>
...
...
@@ -50,7 +50,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"
9.45
"
/>
<result
status=
"timeout"
time=
"
10.09
"
/>
</proof>
<proof
prover=
"1"
...
...
@@ -66,14 +66,14 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
name=
"G2"
locfile=
"check-builtin/euclideandivision/../euclideandivision.why"
loclnum=
"4"
loccnumb=
"12"
loccnume=
"14"
sum=
"
24ab638db2f4cd2b0ad27a15918707d1
"
sum=
"
eeac5b4c0d8433540bfca1c4d506ff93
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =adivc10c3c3"
>
...
...
@@ -91,7 +91,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"
9.26
"
/>
<result
status=
"timeout"
time=
"
10.12
"
/>
</proof>
<proof
prover=
"1"
...
...
@@ -107,7 +107,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
</theory>
...
...
examples/programs/bellman_ford/why3session.xml
View file @
b4a01678
This diff is collapsed.
Click to expand it.
examples/programs/fibonacci/why3session.xml
View file @
b4a01678
...
...
@@ -180,7 +180,7 @@
locfile=
"programs/fibonacci/../fibonacci.mlw"
loclnum=
"82"
loccnumb=
"10"
loccnume=
"16"
expl=
"parameter logfib"
sum=
"
3bee82b2160325a15346a5c53057a94b
"
sum=
"
af2b5f734672fc68af3ae8cf5085fa50
"
proved=
"true"
expanded=
"false"
shape=
"iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1iainfix =amodV0c2c0Lainfix +ainfix *V1V1ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix >=adivV0c2c0Aainfix <adivV0c2V0Aainfix <=c0V0Iainfix >=V0c0F"
>
...
...
@@ -195,7 +195,7 @@
locfile=
"programs/fibonacci/../fibonacci.mlw"
loclnum=
"82"
loccnumb=
"10"
loccnume=
"16"
expl=
"normal postcondition"
sum=
"
1d3cd60f1327fd53ef9954e16c41d661
"
sum=
"
8a0877570abd98ff384c099467c9af87
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix >=V0c0F"
>
...
...
@@ -239,7 +239,7 @@
locfile=
"programs/fibonacci/../fibonacci.mlw"
loclnum=
"82"
loccnumb=
"10"
loccnume=
"16"
expl=
"precondition"
sum=
"
71af7c58a810381aec2d991e4ab91892
"
sum=
"
aa72285b9a0aba886c2356be1a58bfb3
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=adivV0c2c0Aainfix <adivV0c2V0Aainfix <=c0V0Iainfix =V0c0NIainfix >=V0c0F"
>
...
...
@@ -267,7 +267,7 @@
locfile=
"programs/fibonacci/../fibonacci.mlw"
loclnum=
"82"
loccnumb=
"10"
loccnume=
"16"
expl=
"normal postcondition"
sum=
"
0f7cfed40374362fe53b6e53b5ab5968
"
sum=
"
8c7d079fe455dd07faea9fb9774fa739
"
proved=
"true"
expanded=
"false"
shape=
"iainfix =amodV0c2c0Lainfix +ainfix *V1V1ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix >=adivV0c2c0Aainfix <adivV0c2V0Aainfix <=c0V0Iainfix =V0c0NIainfix >=V0c0F"
>
...
...
@@ -280,7 +280,7 @@
edited=
"fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
7
4"
/>
<result
status=
"valid"
time=
"0.
6
4"
/>
</proof>
</goal>
</transf>
...
...
@@ -289,7 +289,7 @@
name=
"fib_m"
locfile=
"programs/fibonacci/../fibonacci.mlw"
loclnum=
"105"
loccnumb=
"8"
loccnume=
"13"
sum=
"
d1c53d543ada9827021c2406c765ac18
"
sum=
"
6be685f947bbf6ff914cf7b797da8e40
"
proved=
"true"
expanded=
"true"
shape=
"Lapoweram1110V0ainfix =afibV0aa21V1Aainfix =afibainfix +V0c1aa11V1Iainfix >=V0c0F"
>
...
...
@@ -300,7 +300,7 @@
edited=
"fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.5
8
"
/>
<result
status=
"valid"
time=
"0.5
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -308,7 +308,7 @@
locfile=
"programs/fibonacci/../fibonacci.mlw"
loclnum=
"109"
loccnumb=
"6"
loccnume=
"10"
expl=
"parameter fibo"
sum=
"
fd564a2ba8960a780506cf3bdb4fb943
"
sum=
"
9ba50c4d5debe897eb4d8392df4e3767
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V2afibV0Iainfix =apoweramk tc1c1c1c0V0amk tainfix +V1V2V2V2V1FAainfix >=V0c0Iainfix >=V0c0F"
>
...
...
@@ -328,7 +328,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
1
"
/>
<result
status=
"valid"
time=
"0.0
0
"
/>
</proof>
</goal>
</theory>
...
...
examples/programs/gcd/why3session.xml
View file @
b4a01678
...
...
@@ -33,7 +33,7 @@
locfile=
"programs/gcd/../gcd.mlw"
loclnum=
"10"
loccnumb=
"10"
loccnume=
"13"
expl=
"parameter gcd"
sum=
"
d8c4bc6f48381e84e04969b311efba00
"
sum=
"
ee0331fbe5f24a27b4018299031d61f2
"
proved=
"true"
expanded=
"true"
shape=
"iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -48,7 +48,7 @@
locfile=
"programs/gcd/../gcd.mlw"
loclnum=
"10"
loccnumb=
"10"
loccnume=
"13"
expl=
"normal postcondition"
sum=
"
d5f9c6d980a45600967f0cbd467afea2
"
sum=
"
2a40bdf2b1e61c0bd97420a5488ad5f6
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -84,7 +84,7 @@
locfile=
"programs/gcd/../gcd.mlw"
loclnum=
"10"
loccnumb=
"10"
loccnume=
"13"
expl=
"precondition"
sum=
"
ba5000dd7ab2a92ea5138c6f3d3950c
d"
sum=
"
e879da4534efea7914866399ee06d1f
d"
proved=
"true"
expanded=
"true"
shape=
"ainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -112,7 +112,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
06
"
/>
<result
status=
"valid"
time=
"0.
21
"
/>
</proof>
</goal>
<goal
...
...
@@ -120,7 +120,7 @@
locfile=
"programs/gcd/../gcd.mlw"
loclnum=
"10"
loccnumb=
"10"
loccnume=
"13"
expl=
"normal postcondition"
sum=
"
92c5d9f0fadcfcaedc9ffd9ccc7e8bd2
"
sum=
"
7fb0be277b7002208d05d13902184f98
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =agcdV1amodV0V1agcdV0V1Iainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -133,7 +133,7 @@
edited=
"gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
68
"
/>
<result
status=
"valid"
time=
"0.
57
"
/>
</proof>
</goal>
</transf>
...
...
examples/programs/gcd_bezout/why3session.xml
View file @
b4a01678
...
...
@@ -29,7 +29,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
b902608a56a4e87fdc894d9ba0c73395
"
sum=
"
26729895440b8b17af6a8da107e15f7a
"
proved=
"true"
expanded=
"true"
shape=
"iainfix >V6c0ainfix <V9V6Aainfix <=c0V6Aainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6Fainfix =ainfix +ainfix *V14V0ainfix *V15V1V7EAainfix =V7agcdV0V1Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFAainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -44,7 +44,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"loop invariant init"
sum=
"
5235bb68096addff97b99a495f3e92d2
"
sum=
"
1d5ad430117a9afe40c20ca9a4a9ee1e
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -56,7 +56,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -64,7 +64,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"loop invariant preservation"
sum=
"4
df161d8c53568375be7e7dea9b2e199
"
sum=
"4
2bf0c3437c23fe281e2a5c5cbbd1c31
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -79,7 +79,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
8e1cc1854f856381dab4fbfec4cb13da
"
sum=
"
4046db3493c6a76f8a5ef45396457f8b
"
proved=
"true"
expanded=
"true"
shape=
"ainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -91,7 +91,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -99,7 +99,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -107,7 +107,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
f3b43220fc3e43850f16ee605e8c9b9e
"
sum=
"
75f86dff9dec98a1867296da6ceb4c35
"
proved=
"true"
expanded=
"true"
shape=
"ainfix >=V9c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -135,7 +135,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
41636bf746068fabd34cb9461499074e
"
sum=
"
2fcc58d1e378790769e9ecf9b3d65b99
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =agcdV8V9agcdV0V1Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -148,7 +148,7 @@
edited=
"gcd_bezout_WP_GcdBezout_WP_parameter_gcd_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
72
"
/>
<result
status=
"valid"
time=
"0.
59
"
/>
</proof>
</goal>
<goal
...
...
@@ -156,7 +156,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
4e322cbd78095100c0f168c5f10a205f
"
sum=
"
13f88960792ae6c94b836cbf15d50e43
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -168,7 +168,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -176,7 +176,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -184,7 +184,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
60d9313c34d31942e589a4a7fc402647
"
sum=
"
499799de664a0bdc7327d8b881567253
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -206,7 +206,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"loop variant decreases"
sum=
"
8d608c4a92e
ce
9
ff
4dfbf0152062a33e
"
sum=
"
c0ad414d661c0d08926e59
ceff
378121
"
proved=
"true"
expanded=
"true"
shape=
"ainfix <V9V6Aainfix <=c0V6Iainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -218,7 +218,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
1
0"
/>
<result
status=
"valid"
time=
"0.0
8
"
/>
</proof>
</goal>
<goal
...
...
@@ -226,7 +226,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"normal postcondition"
sum=
"
4f09b17bc934dd036d55738af2d4c440
"
sum=
"
5526411afdb4989a71227d1d91498fd1
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EAainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -241,7 +241,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"6
d12895b4aaa206efd052ce361bc46b8
"
sum=
"6
71e2a70b74ddad9eb257aa5bd2102ef
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -261,7 +261,7 @@
locfile=
"programs/gcd_bezout/../gcd_bezout.mlw"
loclnum=
"11"
loccnumb=
"6"
loccnume=
"9"
expl=
"parameter gcd"
sum=
"
967cba487e0da4fbd8b770c5a29af08a
"
sum=
"
0ce7a23873c20692b61524b1946ad3dc
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EIainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF"
>
...
...
@@ -273,7 +273,7 @@
memlimit=
"0"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</proof>
</goal>
</transf>
...
...
examples/programs/knuth_prime_numbers/why3session.xml
View file @
b4a01678
This diff is collapsed.
Click to expand it.
examples/tests-provers/alt-ergo-models/why3session.xml
View file @
b4a01678
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name=
"alt-ergo-models/why3session.xml"
>
name=
"
tests-provers/
alt-ergo-models/why3session.xml"
>
<prover
id=
"0"
name=
"Alt-Ergo"
...
...
@@ -12,13 +12,13 @@
expanded=
"true"
>
<theory
name=
"WP M1"
locfile=
"alt-ergo-models/../alt-ergo-models.mlw"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.mlw"
loclnum=
"12"
loccnumb=
"7"
loccnume=
"9"
verified=
"false"
expanded=
"true"
>
<goal
name=
"WP_parameter f"
locfile=
"alt-ergo-models/../alt-ergo-models.mlw"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"7"
expl=
"normal postcondition"
sum=
"a0d81048eafffca9c2034507529acd5c"
...
...
@@ -38,7 +38,7 @@
</goal>
<goal
name=
"WP_parameter f_no_lab"
locfile=
"alt-ergo-models/../alt-ergo-models.mlw"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.mlw"
loclnum=
"21"
loccnumb=
"6"
loccnume=
"14"
expl=
"normal postcondition"
sum=
"f840017f45e1c7b3f0532b46b9c8d8a6"
...
...
@@ -58,7 +58,7 @@
</goal>
<goal
name=
"WP_parameter g"
locfile=
"alt-ergo-models/../alt-ergo-models.mlw"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.mlw"
loclnum=
"28"
loccnumb=
"6"
loccnume=
"7"
expl=
"parameter g"
sum=
"044c6d04c9bbd10bd6ec37d09f41f130"
...
...
@@ -84,13 +84,13 @@
expanded=
"true"
>
<theory
name=
"T"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"2"
loccnumb=
"7"
loccnume=
"8"
verified=
"false"
expanded=
"true"
>
<goal
name=
"g_no_lab"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"6"
loccnumb=
"7"
loccnume=
"15"
sum=
"5db0341ac76573a664138d873f2ee0cc"
proved=
"false"
...
...
@@ -107,7 +107,7 @@
</goal>
<goal
name=
"g_lab0"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"8"
loccnumb=
"7"
loccnume=
"13"
sum=
"8e9074693748b23939e9490537b3a1de"
proved=
"false"
...
...
@@ -124,7 +124,7 @@
</goal>
<goal
name=
"g_lab1"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"11"
loccnumb=
"7"
loccnume=
"13"
sum=
"733127c7327e72652e8d2ad71f0740cb"
proved=
"false"
...
...
@@ -141,7 +141,7 @@
</goal>
<goal
name=
"g2_lab"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"16"
loccnumb=
"7"
loccnume=
"13"
sum=
"3eba6df3534bc325081d7e9f0bf07e60"
proved=
"false"
...
...
@@ -159,13 +159,13 @@
</theory>
<theory
name=
"ModelInt"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"21"
loccnumb=
"7"
loccnume=
"15"
verified=
"false"
expanded=
"true"
>
<goal
name=
"test0"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"25"
loccnumb=
"5"
loccnume=
"10"
sum=
"506786d5b76e4f02e4466d0cc12354c1"
proved=
"true"
...
...
@@ -182,7 +182,7 @@
</goal>
<goal
name=
"test1"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"27"
loccnumb=
"5"
loccnume=
"10"
sum=
"53464dc8479872702159c917f9150dcb"
proved=
"false"
...
...
@@ -199,9 +199,9 @@
</goal>
<goal
name=
"test2"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"31"
loccnumb=
"5"
loccnume=
"10"
sum=
"
5e6dca613e5db62a2fdf2660ff535582
"
sum=
"
ac0b8ab8efcbf6efb912cf860c67226a
"
proved=
"false"
expanded=
"true"
shape=
"ainfix =adivV0V0c1F"
>
...
...
@@ -216,9 +216,9 @@
</goal>
<goal
name=
"test_overflow"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"33"
loccnumb=
"5"
loccnume=
"18"
sum=
"
5d70de2b9f923a914310574254fad74c
"
sum=
"
ba3dbf9bbf606f15444c680293031631
"
proved=
"false"
expanded=
"true"
shape=
"ainfix <=ainfix +V0V1c65535Aainfix <=c0ainfix +V0V1Iainfix <=V1c65535Aainfix <=c0V1Aainfix <=V0c65535Aainfix <=c0V0F"
>
...
...
@@ -233,9 +233,9 @@
</goal>
<goal
name=
"test_overflow2"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"37"
loccnumb=
"5"
loccnume=
"19"
sum=
"
f28b1eb3470cc50ea0c3650f107aab27
"
sum=
"
64151eb0854a02fc3fe96906c002e99f
"
proved=
"false"
expanded=
"true"
shape=
"ainfix <=ainfix +V0V1c65535Aainfix <=aprefix -c2ainfix +V0V1Iainfix <=V1c65535Aainfix <=aprefix -c2V1Aainfix <=V0c65535Aainfix <=aprefix -c2V0F"
>
...
...
@@ -250,9 +250,9 @@
</goal>
<goal
name=
"test_overflow_int16"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"43"
loccnumb=
"5"
loccnume=
"24"
sum=
"
f4e36e34b57f8458e7eb85dcd46be19d
"
sum=
"
693c96dbeef6061cb6ba7c030ef7328b
"
proved=
"false"
expanded=
"true"
shape=
"ais_int16ainfix +V0V1Iais_int16V1Aais_int16V0F"
>
...
...
@@ -262,14 +262,14 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.0
1
"
/>
<result
status=
"unknown"
time=
"0.0
0
"
/>
</proof>
</goal>
<goal
name=
"test_overflow_int16_alt"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"47"
loccnumb=
"5"
loccnume=
"28"
sum=
"
bafb05d844a12e49d8d4e4837e79bde9
"
sum=
"
0cce58e3ea17bb2b49550fbe6cf52561
"
proved=
"false"
expanded=
"true"
shape=
"ainfix <=ainfix +V0V1c65535Aainfix <=aprefix -c65536ainfix +V0V1Iainfix <=V1c65535Aainfix <=aprefix -c65536V1Aainfix <=V0c65535Aainfix <=aprefix -c65536V0F"
>
...
...
@@ -284,9 +284,9 @@
</goal>
<goal
name=
"test_overflow_int16_bis"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"51"
loccnumb=
"5"
loccnume=
"28"
sum=
"
7a83759f576461a70e4afa006e71c6b7
"
sum=
"
f78883ffeac38bd9e171cdadb56e6936
"
proved=
"false"
expanded=
"true"
shape=
"ais_int16ainfix +V0V1Iainfix <=V0V1Aainfix <=c0V0Aais_int16V1Aais_int16V0F"
>
...
...
@@ -301,9 +301,9 @@
</goal>
<goal
name=
"test_overflow_int32"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"58"
loccnumb=
"5"
loccnume=
"24"
sum=
"
c158b0c5a8c2a1438c120ee61ebfbbf9
"
sum=
"
81123038591eb50acc1b2fcd99bf1850
"
proved=
"false"
expanded=
"true"
shape=
"ais_int32ainfix +V0V1Iais_int32V1Aais_int32V0F"
>
...
...
@@ -313,14 +313,14 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.0
0
"
/>
<result
status=
"unknown"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
name=
"test_overflow_int32_bis"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"62"
loccnumb=
"5"
loccnume=
"28"
sum=
"
13278d5c6d1dc5f97c0ad379062d2771
"
sum=
"
dfdd72fd2c80c87b81b6a1612628e7f5
"
proved=
"false"
expanded=
"true"
shape=
"ais_int32ainfix +V0V1Iainfix <=V0V1Aainfix <=c0V0Aais_int32V1Aais_int32V0F"
>
...
...
@@ -335,9 +335,9 @@
</goal>
<goal
name=
"test_overflow_int32_bis_inline"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"66"
loccnumb=
"5"
loccnume=
"35"
sum=
"
f1f6b030b87db2b3aab57752ffac373f
"
sum=
"
3f5aec63a5d3afea5c53daf0fa652e53
"
proved=
"false"
expanded=
"false"
shape=
"ainfix <=ainfix +V0V1c2147483647Aainfix <=aprefix -c2147483648ainfix +V0V1Iainfix <=V0V1Aainfix <=c0V0Aainfix <=V1c2147483647Aainfix <=aprefix -c2147483648V1Aainfix <=V0c2147483647Aainfix <=aprefix -c2147483648V0F"
>
...
...
@@ -353,13 +353,13 @@
</theory>
<theory
name=
"ModelReal"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"72"
loccnumb=
"7"
loccnume=
"16"
verified=
"false"
expanded=
"true"
>
<goal
name=
"test1"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"76"
loccnumb=
"5"
loccnume=
"10"
sum=
"eca61bb8da58aab53b390824efa6096c"
proved=
"false"
...
...
@@ -376,7 +376,7 @@
</goal>
<goal
name=
"test2"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"78"
loccnumb=
"5"
loccnume=
"10"
sum=
"1db3567ffd1099c47db86de68de8b9ce"
proved=
"false"
...
...
@@ -394,13 +394,13 @@
</theory>
<theory
name=
"ModelArray"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"82"
loccnumb=
"7"
loccnume=
"17"
verified=
"false"
expanded=
"true"
>
<goal
name=
"t1"
locfile=
"alt-ergo-models/../alt-ergo-models.why"
locfile=
"
tests-provers/
alt-ergo-models/../alt-ergo-models.why"
loclnum=
"86"
loccnumb=
"5"
loccnume=
"7"
sum=
"80ac2844addd3bc5d617d1bfe18cfa0f"
proved=
"false"
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment