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
8d3f825a
Commit
8d3f825a
authored
Jun 05, 2014
by
Jean-Christophe Filliâtre
Browse files
no need for lemma fib_pos
parent
fc9137e8
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/fibonacci.mlw
View file @
8d3f825a
...
...
@@ -92,6 +92,7 @@ module SmallestFibAbove
let b = ref 1 in
while !b <= x do
invariant { exists k: int. 0 <= k /\ !a = fib k <= x /\ !b = fib (k+1) }
invariant { 0 <= !a /\ 1 <= !b }
variant { 2*x - (!a + !b) }
let f = !a + !b in
a := !b;
...
...
examples/fibonacci/why3session.xml
View file @
8d3f825a
...
...
@@ -55,7 +55,7 @@
name=
"isfib_2_1"
locfile=
"../fibonacci.mlw"
loclnum=
"6"
loccnumb=
"8"
loccnume=
"17"
sum=
"
925a4ee99401641fc90c3f54afbfcd23
"
sum=
"
15aab3978bc62f481e12635752c9bc36
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =afibc2c1"
>
...
...
@@ -72,7 +72,7 @@
name=
"isfib_6_8"
locfile=
"../fibonacci.mlw"
loclnum=
"7"
loccnumb=
"8"
loccnume=
"17"
sum=
"
687cb7ce6b0d102f14a35a6eb228bedb
"
sum=
"
dfb0ce3fd8b846f274e9692059e947b8
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =afibc6c8"
>
...
...
@@ -89,7 +89,7 @@
name=
"not_isfib_2_2"
locfile=
"../fibonacci.mlw"
loclnum=
"9"
loccnumb=
"8"
loccnume=
"21"
sum=
"
9
3d
096d7fc047e0c8a12f90c2cfb562b
"
sum=
"
e
3d
5312d3d038b8ee04543dcda0ea242
"
proved=
"true"
expanded=
"false"
shape=
"Nainfix =afibc2c2"
>
...
...
@@ -146,7 +146,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"19"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for fib"
sum=
"c
d7b580ac0e3942c73b2773e8938cf87
"
sum=
"c
33a40a92865042be99b0ff3d2abfc60
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =afibV0V3Iainfix =afibainfix +V1c1V3Aainfix =afibainfix +ainfix +V1c1c1V2Aainfix <=ainfix +V1c1V0Aainfix <=c0ainfix +V1c1Aainfix =afibainfix +V4c1V5Aainfix =afibainfix +ainfix +V4c1c1V6Aainfix <=ainfix +V4c1V0Aainfix <=c0ainfix +V4c1Iainfix =V6ainfix +V2V3FIainfix =V5V2FIainfix =afibV4V3Aainfix =afibainfix +V4c1V2Aainfix <=V4V0Aainfix <=c0V4Iainfix <=V4V1Aainfix <=c0V4FFAainfix =afibc0c0Aainfix =afibainfix +c0c1c1Aainfix <=c0V0Aainfix <=c0c0Iainfix <=c0V1Aainfix =afibV0c0Iainfix >c0V1Lainfix -V0c1Iainfix >=V0c0F"
>
...
...
@@ -175,7 +175,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"39"
loccnumb=
"10"
loccnume=
"17"
expl=
"VC for fib_aux"
sum=
"
272e2024e8aae95e4a86112c0efd9d04
"
sum=
"
fa0648e548246a24e329cc43cbc2dd79
"
proved=
"true"
expanded=
"false"
shape=
"iainfix =afibainfix +V5V4afibainfix +V0V3Aainfix =ainfix +V1V2afibainfix +V5c1Aainfix =V2afibV5Aainfix <=c0V5Aainfix >=V4c0Aainfix <V4V3Aainfix <=c0V3Lainfix +V0c1Lainfix -V3c1ainfix =V1afibainfix +V0V3ainfix =V3c0Iainfix =V2afibainfix +V0c1Aainfix =V1afibV0Aainfix <=c0V0Aainfix >=V3c0F"
>
...
...
@@ -190,7 +190,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"39"
loccnumb=
"10"
loccnume=
"17"
expl=
"1. postcondition"
sum=
"
b85ace9c2b3cd3973aa0fdacc2b7f08f
"
sum=
"
00fd0627e82b0aba30173f5aa459ecfe
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =V1afibainfix +V0V3Iainfix =V3c0Iainfix =V2afibainfix +V0c1Aainfix =V1afibV0Aainfix <=c0V0Aainfix >=V3c0F"
>
...
...
@@ -234,7 +234,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"39"
loccnumb=
"10"
loccnume=
"17"
expl=
"2. variant decrease"
sum=
"
8d96dc79ae0f21266697da79fe040ea4
"
sum=
"
cc6362fe1bd185bb34d04a9aecc0e420
"
proved=
"true"
expanded=
"false"
shape=
"variant decreaseainfix <V4V3Aainfix <=c0V3Lainfix +V0c1Lainfix -V3c1INainfix =V3c0Iainfix =V2afibainfix +V0c1Aainfix =V1afibV0Aainfix <=c0V0Aainfix >=V3c0F"
>
...
...
@@ -278,7 +278,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"39"
loccnumb=
"10"
loccnume=
"17"
expl=
"3. precondition"
sum=
"
859f6fe6cd7a13133c50b262a8ce7284
"
sum=
"
99f1517a0e3c2ad76a5c9cf01ab1b4f9
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >=V4c0Lainfix +V0c1Lainfix -V3c1INainfix =V3c0Iainfix =V2afibainfix +V0c1Aainfix =V1afibV0Aainfix <=c0V0Aainfix >=V3c0F"
>
...
...
@@ -322,7 +322,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"39"
loccnumb=
"10"
loccnume=
"17"
expl=
"4. precondition"
sum=
"
4a93bf4100d75ebb841c3098a7f61657
"
sum=
"
17d4faa3db0b651e60c6bda7441b0fe6
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix =ainfix +V1V2afibainfix +V5c1Aainfix =V2afibV5Aainfix <=c0V5Lainfix +V0c1Lainfix -V3c1INainfix =V3c0Iainfix =V2afibainfix +V0c1Aainfix =V1afibV0Aainfix <=c0V0Aainfix >=V3c0F"
>
...
...
@@ -358,7 +358,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"39"
loccnumb=
"10"
loccnume=
"17"
expl=
"5. postcondition"
sum=
"
b77f1237c49e5c8d38d4a360056ef4a5
"
sum=
"
46b8a38fcab44f0e75405ae1479315a7
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =afibainfix +V5V4afibainfix +V0V3Iainfix =ainfix +V1V2afibainfix +V5c1Aainfix =V2afibV5Aainfix <=c0V5Aainfix >=V4c0Lainfix +V0c1Lainfix -V3c1INainfix =V3c0Iainfix =V2afibainfix +V0c1Aainfix =V1afibV0Aainfix <=c0V0Aainfix >=V3c0F"
>
...
...
@@ -404,7 +404,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"46"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for fib"
sum=
"
f85d4d44b9fd1b214503cea742dadaf0
"
sum=
"
02ca6fb4801985c3dcfbb97275bc862d
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =afibainfix +c0V0afibV0Aainfix =c1afibainfix +c0c1Aainfix =c0afibc0Aainfix <=c0c0Aainfix >=V0c0Iainfix <=c0V0F"
>
...
...
@@ -419,7 +419,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"46"
loccnumb=
"6"
loccnume=
"9"
expl=
"1. precondition"
sum=
"
3592f1e391215230a16f7928872ba060
"
sum=
"
e17a273bc9ac73440011c4f7bfb0dccc
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >=V0c0Iainfix <=c0V0F"
>
...
...
@@ -463,7 +463,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"46"
loccnumb=
"6"
loccnume=
"9"
expl=
"2. precondition"
sum=
"
3a29ac7c64eb28935b1546bee89644d5
"
sum=
"
48df7d6eecd66772f30be09340b2c6ae
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix =c1afibainfix +c0c1Aainfix =c0afibc0Aainfix <=c0c0Iainfix <=c0V0F"
>
...
...
@@ -507,7 +507,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"46"
loccnumb=
"6"
loccnume=
"9"
expl=
"3. postcondition"
sum=
"
a633953ae1d666d03167c8dbdd6799e6
"
sum=
"
96743058293856fce1e97c3d9e6257c2
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =afibainfix +c0V0afibV0Iainfix =c1afibainfix +c0c1Aainfix =c0afibc0Aainfix <=c0c0Aainfix >=V0c0Iainfix <=c0V0F"
>
...
...
@@ -553,7 +553,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"51"
loccnumb=
"6"
loccnume=
"12"
expl=
"VC for test42"
sum=
"
720c76753dddd68ce68dc352b585d907
"
sum=
"
5e16391cd28cc4d718e7ebebb7c1fca2
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <=c0c42"
>
...
...
@@ -597,7 +597,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"55"
loccnumb=
"6"
loccnume=
"11"
expl=
"VC for bench"
sum=
"
a472128007cc714bfd3482c74977d96
7"
sum=
"
98619003152866c935bb2d4fb96d19f
7"
proved=
"true"
expanded=
"false"
shape=
"t"
>
...
...
@@ -650,7 +650,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"65"
loccnumb=
"10"
loccnume=
"17"
expl=
"VC for fib_aux"
sum=
"
6ebc27998f220384c406a6c4a2c8dabb
"
sum=
"
abad0fc6a6c557f10d7cd32e86dc689d
"
proved=
"true"
expanded=
"false"
shape=
"iainfix =V5afibainfix +V6V2Iainfix =V1afibainfix +V6c1Aainfix =V0afibV6Aainfix <=c0V6FIainfix =V5afibainfix +V7V3Iainfix =V4afibainfix +V7c1Aainfix =V1afibV7Aainfix <=c0V7FFAainfix =V4afibainfix +V8c1Aainfix =V1afibV8Aainfix <=c0V8EAainfix >=V3c0Aainfix <V3V2Aainfix <=c0V2Lainfix +V0V1Lainfix -V2c1ainfix =V0afibainfix +V9V2Iainfix =V1afibainfix +V9c1Aainfix =V0afibV9Aainfix <=c0V9Fainfix =V2c0Iainfix =V1afibainfix +V10c1Aainfix =V0afibV10Aainfix <=c0V10EAainfix >=V2c0F"
>
...
...
@@ -665,7 +665,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"65"
loccnumb=
"10"
loccnume=
"17"
expl=
"1. postcondition"
sum=
"
c94bbd87b12a9670f9a8022e9a42a607
"
sum=
"
b05783f4cde7e81581259b310f016e21
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =V0afibainfix +V3V2Iainfix =V1afibainfix +V3c1Aainfix =V0afibV3Aainfix <=c0V3FIainfix =V2c0Iainfix =V1afibainfix +V4c1Aainfix =V0afibV4Aainfix <=c0V4EAainfix >=V2c0F"
>
...
...
@@ -701,7 +701,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"65"
loccnumb=
"10"
loccnume=
"17"
expl=
"2. variant decrease"
sum=
"
a69504a90c7fba606bc92b55126134db
"
sum=
"
fb33f040923d503761f1ac8dd546f5f6
"
proved=
"true"
expanded=
"false"
shape=
"variant decreaseainfix <V3V2Aainfix <=c0V2Lainfix +V0V1Lainfix -V2c1INainfix =V2c0Iainfix =V1afibainfix +V5c1Aainfix =V0afibV5Aainfix <=c0V5EAainfix >=V2c0F"
>
...
...
@@ -737,7 +737,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"65"
loccnumb=
"10"
loccnume=
"17"
expl=
"3. precondition"
sum=
"
949ee5fd8a3f213a0f3a0070458363cc
"
sum=
"
d9536ff5ddafb7d15d52eb86bd12197a
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >=V3c0Lainfix +V0V1Lainfix -V2c1INainfix =V2c0Iainfix =V1afibainfix +V5c1Aainfix =V0afibV5Aainfix <=c0V5EAainfix >=V2c0F"
>
...
...
@@ -773,7 +773,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"65"
loccnumb=
"10"
loccnume=
"17"
expl=
"4. precondition"
sum=
"
12d009a04d1f03eb37f2afbbf79571d4
"
sum=
"
c0ce52b40ff9e1f4732ac54dd461baff
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix =V4afibainfix +V5c1Aainfix =V1afibV5Aainfix <=c0V5ELainfix +V0V1Lainfix -V2c1INainfix =V2c0Iainfix =V1afibainfix +V6c1Aainfix =V0afibV6Aainfix <=c0V6EAainfix >=V2c0F"
>
...
...
@@ -809,7 +809,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"65"
loccnumb=
"10"
loccnume=
"17"
expl=
"5. postcondition"
sum=
"
27a6748beaf6886f15113529a464619c
"
sum=
"
ff1ab0dd98aa0b297144ad03625a66b1
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =V5afibainfix +V6V2Iainfix =V1afibainfix +V6c1Aainfix =V0afibV6Aainfix <=c0V6FIainfix =V5afibainfix +V7V3Iainfix =V4afibainfix +V7c1Aainfix =V1afibV7Aainfix <=c0V7FFIainfix =V4afibainfix +V8c1Aainfix =V1afibV8Aainfix <=c0V8EAainfix >=V3c0Lainfix +V0V1Lainfix -V2c1INainfix =V2c0Iainfix =V1afibainfix +V9c1Aainfix =V0afibV9Aainfix <=c0V9EAainfix >=V2c0F"
>
...
...
@@ -847,7 +847,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"73"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for fib"
sum=
"
6c6973b71b2d5bff61e0c885ce5029b8
"
sum=
"
fc98a2f8a69c57ab706329a0a35ffad1
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V1afibV0Iainfix =V1afibainfix +V2V0Iainfix =c1afibainfix +V2c1Aainfix =c0afibV2Aainfix <=c0V2FFAainfix =c1afibainfix +V3c1Aainfix =c0afibV3Aainfix <=c0V3EAainfix >=V0c0Iainfix <=c0V0F"
>
...
...
@@ -862,7 +862,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"73"
loccnumb=
"6"
loccnume=
"9"
expl=
"1. precondition"
sum=
"
3592f1e391215230a16f7928872ba060
"
sum=
"
e17a273bc9ac73440011c4f7bfb0dccc
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >=V0c0Iainfix <=c0V0F"
>
...
...
@@ -898,7 +898,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"73"
loccnumb=
"6"
loccnume=
"9"
expl=
"2. precondition"
sum=
"
aa3447bedb5e904d052ee8d5dfabcfb7
"
sum=
"
9ce4e6725a3871813a57389b515de01e
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix =c1afibainfix +V1c1Aainfix =c0afibV1Aainfix <=c0V1EIainfix <=c0V0F"
>
...
...
@@ -934,7 +934,7 @@
locfile=
"../fibonacci.mlw"
loclnum=
"73"
loccnumb=
"6"
loccnume=
"9"
expl=
"3. postcondition"
sum=
"
98b74ea661c0935fe544dd409c2a5b67
"
sum=
"
c7a286f86f334aa5518b7efcffd82835
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =V1afibV0Iainfix =V1afibainfix +V2V0Iainfix =c1afibainfix +V2c1Aainfix =c0afibV2Aainfix <=c0V2FFIainfix =c1afibainfix +V3c1Aainfix =c0afibV3Aainfix <=c0V3EAainfix >=V0c0Iainfix <=c0V0F"
>
...
...
@@ -973,16 +973,16 @@
locfile=
"../fibonacci.mlw"
loclnum=
"80"
loccnumb=
"7"
loccnume=
"23"
verified=
"true"
expanded=
"
fals
e"
>
expanded=
"
tru
e"
>
<goal
name=
"WP_parameter smallest_fib_above"
locfile=
"../fibonacci.mlw"
loclnum=
"87"
loccnumb=
"6"
loccnume=
"24"
expl=
"VC for smallest_fib_above"
sum=
"
2cb037e236a8b011db9f700e744e18ce
"
sum=
"
c69813f51ecfc06184cca298b1f8cdf8
"
proved=
"true"
expanded=
"
fals
e"
shape=
"iainfix =afibainfix +V3c1V1Aainfix <V0afibainfix +V3c1Aainfix <=afibV3V0Aainfix <=c0V3Eainfix <ainfix -ainfix *c2V0ainfix +V4V5ainfix -ainfix *c2V0ainfix +V2V1Aainfix <=c0ainfix -ainfix *c2V0ainfix +V2V1Aainfix =V5afibainfix +V6c1Aainfix <=afibV6V0Aainfix =V4afibV6Aainfix <=c0V6EIainfix =V5ainfix +V2V1FIainfix =V4V1Fainfix <=V1V0Iainfix =V1afibainfix +V7c1Aainfix <=afibV7V0Aainfix =V2afibV7Aainfix <=c0V7EFAainfix =c1afibainfix +V8c1Aainfix <=afibV8V0Aainfix =c0afibV8Aainfix <=c0V8EIainfix <=c0V0F"
>
expanded=
"
tru
e"
shape=
"iainfix =afibainfix +V3c1V1Aainfix <V0afibainfix +V3c1Aainfix <=afibV3V0Aainfix <=c0V3Eainfix <ainfix -ainfix *c2V0ainfix +V4V5ainfix -ainfix *c2V0ainfix +V2V1Aainfix <=c0ainfix -ainfix *c2V0ainfix +V2V1Aainfix
<=c1V5Aainfix <=c0V4Aainfix
=V5afibainfix +V6c1Aainfix <=afibV6V0Aainfix =V4afibV6Aainfix <=c0V6EIainfix =V5ainfix +V2V1FIainfix =V4V1Fainfix <=V1V0Iainfix
<=c1V1Aainfix <=c0V2Aainfix
=V1afibainfix +V7c1Aainfix <=afibV7V0Aainfix =V2afibV7Aainfix <=c0V7EFAainfix
<=c1c1Aainfix <=c0c0Aainfix
=c1afibainfix +V8c1Aainfix <=afibV8V0Aainfix =c0afibV8Aainfix <=c0V8EIainfix <=c0V0F"
>
<label
name=
"expl:VC for smallest_fib_above"
/>
<proof
...
...
@@ -998,7 +998,7 @@
<theory
name=
"Mat22"
locfile=
"../fibonacci.mlw"
loclnum=
"10
4
"
loccnumb=
"7"
loccnume=
"12"
loclnum=
"10
5
"
loccnumb=
"7"
loccnume=
"12"
verified=
"true"
expanded=
"true"
>
<label
...
...
@@ -1007,15 +1007,15 @@
<theory
name=
"FibonacciLogarithmic"
locfile=
"../fibonacci.mlw"
loclnum=
"12
6
"
loccnumb=
"7"
loccnume=
"27"
loclnum=
"12
7
"
loccnumb=
"7"
loccnume=
"27"
verified=
"true"
expanded=
"
fals
e"
>
expanded=
"
tru
e"
>
<goal
name=
"WP_parameter logfib"
locfile=
"../fibonacci.mlw"
loclnum=
"14
0
"
loccnumb=
"10"
loccnume=
"16"
loclnum=
"14
1
"
loccnumb=
"10"
loccnume=
"16"
expl=
"VC for logfib"
sum=
"
126e157d6837d90d7ca1d2c39fc15946
"
sum=
"
d4dd7dccf6c1b8fab720f436a541a77a
"
proved=
"true"
expanded=
"false"
shape=
"iiainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *V4V4ainfix *V3V3Lainfix *V3ainfix +V2V4ainfix =apoweramk tc1c1c1c0V0amk tainfix +V7V8V8V8V7Lainfix *V3ainfix +V2V4Lainfix +ainfix *V2V2ainfix *V3V3ainfix =amodV0c2c0Lainfix +V2V3Iainfix =apoweramk tc1c1c1c0V1amk tainfix +V2V3V3V3V2FAainfix >=V1c0Aainfix <V1V0Aainfix <=c0V0LadivV0c2ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1ainfix =V0c0Iainfix >=V0c0F"
>
...
...
@@ -1028,9 +1028,9 @@
<goal
name=
"WP_parameter logfib.1"
locfile=
"../fibonacci.mlw"
loclnum=
"14
0
"
loccnumb=
"10"
loccnume=
"16"
loclnum=
"14
1
"
loccnumb=
"10"
loccnume=
"16"
expl=
"1. postcondition"
sum=
"
d9e2058f51f7f70b0fc5f3651c3011d
5"
sum=
"
69cb2f091b3a66334b2aacb49a0456e
5"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix >=V0c0F"
>
...
...
@@ -1072,9 +1072,9 @@
<goal
name=
"WP_parameter logfib.2"
locfile=
"../fibonacci.mlw"
loclnum=
"14
0
"
loccnumb=
"10"
loccnume=
"16"
loclnum=
"14
1
"
loccnumb=
"10"
loccnume=
"16"
expl=
"2. variant decrease"
sum=
"
7b4751224a113953fa682886e588ff21
"
sum=
"
a6278a43b357e52386379de92b22d9c4
"
proved=
"true"
expanded=
"false"
shape=
"variant decreaseainfix <V1V0Aainfix <=c0V0LadivV0c2INainfix =V0c0Iainfix >=V0c0F"
>
...
...
@@ -1092,9 +1092,9 @@
<goal
name=
"WP_parameter logfib.3"
locfile=
"../fibonacci.mlw"
loclnum=
"14
0
"
loccnumb=
"10"
loccnume=
"16"
loclnum=
"14
1
"
loccnumb=
"10"
loccnume=
"16"
expl=
"3. precondition"
sum=
"
9be9870b5f37ba23b1ccf49bf6cb01d3
"
sum=
"
3f33fa6a056926fc563ba658c8f13f22
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >=V1c0LadivV0c2INainfix =V0c0Iainfix >=V0c0F"
>
...
...
@@ -1120,9 +1120,9 @@
<goal
name=
"WP_parameter logfib.4"
locfile=
"../fibonacci.mlw"
loclnum=
"14
0
"
loccnumb=
"10"
loccnume=
"16"
loclnum=
"14
1
"
loccnumb=
"10"
loccnume=
"16"
expl=
"4. postcondition"
sum=
"
972281e314038bd2c3ef9b4ed4f6be0d
"
sum=
"
7b7a848fd3c85b5823edf5084297bfd1
"
proved=
"true"
expanded=
"false"
shape=
"postconditioniainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *V4V4ainfix *V3V3Lainfix *V3ainfix +V2V4ainfix =apoweramk tc1c1c1c0V0amk tainfix +V7V8V8V8V7Lainfix *V3ainfix +V2V4Lainfix +ainfix *V2V2ainfix *V3V3ainfix =amodV0c2c0Lainfix +V2V3Iainfix =apoweramk tc1c1c1c0V1amk tainfix +V2V3V3V3V2FIainfix >=V1c0LadivV0c2INainfix =V0c0Iainfix >=V0c0F"
>
...
...
@@ -1143,8 +1143,8 @@
<goal
name=
"fib_m"
locfile=
"../fibonacci.mlw"
loclnum=
"16
3
"
loccnumb=
"8"
loccnume=
"13"
sum=
"f
6032cadecf01184ee3b2499de34fbc
1"
loclnum=
"16
4
"
loccnumb=
"8"
loccnume=
"13"
sum=
"f
4108c167ac378dc0bb2fbb56847e07
1"
proved=
"true"
expanded=
"false"
shape=
"ainfix =afibV0aa21V1Aainfix =afibainfix +V0c1aa11V1Lapoweram1110V0Iainfix >=V0c0F"
>
...
...
@@ -1161,9 +1161,9 @@
<goal
name=
"WP_parameter fibo"
locfile=
"../fibonacci.mlw"
loclnum=
"16
7
"
loccnumb=
"6"
loccnume=
"10"
loclnum=
"16
8
"
loccnumb=
"6"
loccnume=
"10"
expl=
"VC for fibo"
sum=
"
08212151ec4ab46d1c07ec046dfc7de0
"
sum=
"
38ae29d3fc4fbfcdd946e1d92ff141b8
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V2afibV0Iainfix =apoweramk tc1c1c1c0V0amk tainfix +V1V2V2V2V1FAainfix >=V0c0Iainfix >=V0c0F"
>
...
...
@@ -1189,9 +1189,9 @@
<goal
name=
"WP_parameter test0"
locfile=
"../fibonacci.mlw"
loclnum=
"17
1
"
loccnumb=
"6"
loccnume=
"11"
loclnum=
"17
2
"
loccnumb=
"6"
loccnume=
"11"
expl=
"VC for test0"
sum=
"
871d321a0b6eb51904e5888f00f72a33
"
sum=
"
2ed01e39d6b5ac51495153ba59fe47f4
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=c0c0"
>
...
...
@@ -1209,9 +1209,9 @@
<goal
name=
"WP_parameter test1"
locfile=
"../fibonacci.mlw"
loclnum=
"17
2
"
loccnumb=
"6"
loccnume=
"11"
loclnum=
"17
3
"
loccnumb=
"6"
loccnume=
"11"
expl=
"VC for test1"
sum=
"
aa46903e4241a077651250a270473944
"
sum=
"
4e6f91b5630b53961359e65fde7720bc
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=c1c0"
>
...
...
@@ -1229,9 +1229,9 @@
<goal
name=
"WP_parameter test7"
locfile=
"../fibonacci.mlw"
loclnum=
"17
3
"
loccnumb=
"6"
loccnume=
"11"
loclnum=
"17
4
"
loccnumb=
"6"
loccnume=
"11"
expl=
"VC for test7"
sum=
"
ae
e0
8
ca
f7b139c07463c881b594077ad
"
sum=
"
39498
e0
e
ca
6c3664c87cab69c3a69a21
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=c7c0"
>
...
...
@@ -1249,9 +1249,9 @@
<goal
name=
"WP_parameter test42"
locfile=
"../fibonacci.mlw"
loclnum=
"17
4
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"17
5
"
loccnumb=
"6"
loccnume=
"12"
expl=
"VC for test42"
sum=
"
727974886ff9abcb6113ade884abae06
"
sum=
"
6537eb059d9e6f5fd0a3502e6095fb1f
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=c42c0"
>
...
...
@@ -1269,9 +1269,9 @@
<goal
name=
"WP_parameter test2014"
locfile=
"../fibonacci.mlw"
loclnum=
"17
5
"
loccnumb=
"6"
loccnume=
"14"
loclnum=
"17
6
"
loccnumb=
"6"
loccnume=
"14"
expl=
"VC for test2014"
sum=
"
e3895118f379de77828e2174243976ec
"
sum=
"
12ce06848394595336f904d4128638aa
"
proved=
"true"
expanded=
"false"
shape=
"ainfix >=c2014c0"
>
...
...
@@ -1289,9 +1289,9 @@
<goal
name=
"WP_parameter bench"
locfile=
"../fibonacci.mlw"
loclnum=
"1
79
"
loccnumb=
"6"
loccnume=
"11"
loclnum=
"1
80
"
loccnumb=
"6"
loccnume=
"11"
expl=
"VC for bench"
sum=
"
f5b8f6a19ad2d36e59f8d163bac3b989
"
sum=
"
822f4dbc4c001f31f7a546c376f270a7
"
proved=
"true"
expanded=
"false"
shape=
"t"
>
...
...
theories/int.why
View file @
8d3f825a
...
...
@@ -461,7 +461,5 @@ theory Fibonacci "Fibonacci numbers"
axiom fib1: fib 1 = 1
axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)
lemma fib_pos: forall i: int. 1 <= i -> 0 < fib i
end
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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