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
70c674a3
Commit
70c674a3
authored
Apr 12, 2015
by
Jean-Christophe Filliâtre
Browse files
vstte10_queens: updated proof (WIP)
parent
340ffc11
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/vstte10_queens.mlw
View file @
70c674a3
...
...
@@ -192,6 +192,7 @@ module MachineArithmetic
requires { 0 <= to_int pos <= to_int n }
requires { is_board board (to_int pos) }
variant { to_int n - to_int pos }
ensures { result.O.valid }
ensures { is_board board (to_int pos) }
=
if eq pos n then
...
...
@@ -200,15 +201,15 @@ module MachineArithmetic
let s = { ot = O.zero () } in
let rec forloop (i: int63) = (* for i = 0 to n-1 do *)
requires { 0 <= to_int i <= to_int n }
requires { s.ot.O.valid }
requires { is_board board (to_int pos) }
variant { to_int n - to_int i }
ensures { s.ot.O.valid }
ensures { is_board board (to_int pos) }
if i < n then begin
board[pos] <- i;
if mcheck_is_consistent board pos then
s.ot <- O.add s.ot (mcount_bt_queens board n (pos + of_int 1));
(* let _ = O.add !s (mcount_bt_queens board n (pos + of_int 1))
in (); *)
forloop (i + of_int 1)
end in
forloop (of_int 0);
...
...
examples/vstte10_queens/why3session.xml
View file @
70c674a3
...
...
@@ -50,92 +50,122 @@
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"0"
/></proof>
</goal>
</theory>
<theory
name=
"MachineArithmetic"
sum=
"
0500018a9f9265efb1b389c414cb9813
"
expanded=
"true"
>
<theory
name=
"MachineArithmetic"
sum=
"
5cefdde670c8babce2b61c2fb35e26ba
"
expanded=
"true"
>
<goal
name=
"WP_parameter mcheck_is_consistent"
expl=
"VC for mcheck_is_consistent"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.27"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens"
expl=
"VC for mcount_bt_queens"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter mcount_bt_queens.1"
expl=
"1. p
ost
condition"
>
<proof
prover=
"
4"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens"
expl=
"VC for mcount_bt_queens"
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter mcount_bt_queens.1"
expl=
"1. p
re
condition"
>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.2"
expl=
"2.
index in array bounds
"
>
<goal
name=
"WP_parameter mcount_bt_queens.2"
expl=
"2.
postcondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"15"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.3"
expl=
"3. p
re
condition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"1
7
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.3"
expl=
"3. p
ost
condition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"1
5
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.4"
expl=
"4.
precondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.0
5
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.4"
expl=
"4.
index in array bounds
"
>
<proof
prover=
"
4"
memlimit=
"100
0"
><result
status=
"valid"
time=
"0.0
2"
steps=
"18
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.5"
expl=
"5.
integer overflow
"
>
<goal
name=
"WP_parameter mcount_bt_queens.5"
expl=
"5.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"20"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.6"
expl=
"6.
integer overflow
"
>
<proof
prover=
"
4"
memlimit=
"100
0"
><result
status=
"valid"
time=
"0.0
4"
steps=
"47
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.6"
expl=
"6.
precondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.0
5
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.7"
expl=
"7.
variant decrease
"
>
<goal
name=
"WP_parameter mcount_bt_queens.7"
expl=
"7.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"23"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.8"
expl=
"8.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
2
"
steps=
"
23
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.8"
expl=
"8.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
4
"
steps=
"
50
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.9"
expl=
"9.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"2
3
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.9"
expl=
"9.
variant decrease
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"2
6
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.10"
expl=
"10. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
1
"
steps=
"2
3
"
/></proof>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
2
"
steps=
"2
6
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.11"
expl=
"11.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"2
8
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.11"
expl=
"11.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"2
6
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.12"
expl=
"12.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.1
5
"
steps=
"
6
2"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.12"
expl=
"12.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
0
1"
steps=
"2
6
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.13"
expl=
"13.
variant decreas
e"
>
<goal
name=
"WP_parameter mcount_bt_queens.13"
expl=
"13.
precondition"
expanded=
"tru
e"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"31"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.14"
expl=
"14.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"3
1
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.14"
expl=
"14.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"3
7
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.15"
expl=
"15.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
4
8"
steps=
"
8
1"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.15"
expl=
"15.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
0
8"
steps=
"
7
1"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.16"
expl=
"16.
postcondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
35
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.16"
expl=
"16.
variant decrease
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
40
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.17"
expl=
"17.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
1
"
steps=
"
2
0"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.17"
expl=
"17.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
2
"
steps=
"
4
0"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.18"
expl=
"18.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
8
"
steps=
"4
7
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.18"
expl=
"18.
precondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
3
"
steps=
"4
0
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.19"
expl=
"19.
variant decrease
"
>
<proof
prover=
"
4"
memlimit=
"100
0"
><result
status=
"valid"
time=
"0.0
2"
steps=
"23
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.19"
expl=
"19.
precondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.0
5
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.20"
expl=
"20. p
re
condition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
23
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.20"
expl=
"20. p
ost
condition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
45
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.21"
expl=
"21. p
re
condition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.2
3
"
steps=
"
6
5"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.21"
expl=
"21. p
ost
condition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
0
2"
steps=
"
4
5"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.22"
expl=
"22.
postcondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
2
"
steps=
"2
7
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.22"
expl=
"22.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
1
"
steps=
"2
3
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.23"
expl=
"23.
postcondition
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
0
1"
steps=
"
1
5"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.23"
expl=
"23.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.1
5
"
steps=
"5
0
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.24"
expl=
"24.
integer overflow
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
11
"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.24"
expl=
"24.
variant decrease
"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
26
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.25"
expl=
"25. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
1
2"
/></proof>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"2
6
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.26"
expl=
"26. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"
1
2"
/></proof>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"2
6
"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.27"
expl=
"27. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"15"
/></proof>
<goal
name=
"WP_parameter mcount_bt_queens.27"
expl=
"27. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.48"
steps=
"107"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.28"
expl=
"28. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"31"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.29"
expl=
"29. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"31"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.30"
expl=
"30. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"18"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.31"
expl=
"31. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"18"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.32"
expl=
"32. integer overflow"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"13"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.33"
expl=
"33. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"14"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.34"
expl=
"34. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"14"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.35"
expl=
"35. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"14"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.36"
expl=
"36. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"18"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.37"
expl=
"37. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"18"
/></proof>
</goal>
</transf>
</goal>
...
...
examples/vstte10_queens/why3shapes.gz
View file @
70c674a3
No preview for this file type
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