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
312f137e
Commit
312f137e
authored
Apr 11, 2015
by
Jean-Christophe Filliâtre
Browse files
gallery: some experiments in vstte10_queens to count solutions
parent
20cdf859
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/vstte10_queens.mlw
View file @
312f137e
...
...
@@ -111,4 +111,121 @@ module NQueens
with Solution -> a
end
(** variant: counting solutions (not part of the competition)
TODO: prove soundness i.e. we indeed count the number of solutions *)
use import ref.Refint
let rec count_bt_queens (board: array int) (n: int) (pos: int) : int
variant { n - pos }
requires { length board = n /\ 0 <= pos <= n /\ solution board pos }
ensures { eq_board board (old board) pos }
= 'Init:
if pos = n then
1
else begin
let s = ref 0 in
for i = 0 to n - 1 do
invariant { eq_board board (at board 'Init) pos }
board[pos] <- i;
if check_is_consistent board pos then
s += count_bt_queens board n (pos+1)
done;
!s
end
let count_queens (board: array int) (n: int) : int
requires { length board = n }
ensures { true }
= count_bt_queens board n 0
let test_count_8 () =
let a = Array.make 8 0 in
count_queens a 8
end
(** counting solutions with machine integers *)
module MachineArithmetic
use import ref.Refint
use import mach.array.Array63
use import mach.int.Int63
predicate is_board (board: array int63) (pos: int) =
forall q: int. 0 <= q < pos ->
0 <= to_int board[q] < to_int (length board)
exception MInconsistent int63
let mcheck_is_consistent (board: array int63) (pos: int63)
requires { 0 <= to_int pos < to_int (length board) }
requires { is_board board (to_int pos + 1) }
= try
let rec forloop q (* for q = 0 to pos-1 do *) =
requires { 0 <= to_int q <= to_int pos }
requires { is_board board (to_int pos + 1) }
variant { to_int pos - to_int q }
raises { MInconsistent -> true }
if q < pos then begin
let bq = board[q] in
let bpos = board[pos] in
if bq = bpos then raise (MInconsistent q);
if bq - bpos = pos - q then raise (MInconsistent q);
if bpos - bq = pos - q then raise (MInconsistent q);
forloop (q + of_int 1)
end in
forloop (of_int 0);
True
with MInconsistent _ ->
False
end
use mach.onetime.OneTime as O
(***
let rec mcount_bt_queens (board: array int63) (n: int63) (pos: int63) : O.t
requires { to_int (length board) = to_int n }
requires { 0 <= to_int pos <= to_int n }
requires { is_board board (to_int pos) }
variant { to_int n - to_int pos }
ensures { is_board board (to_int pos) }
=
if eq pos n then
O.succ (O.zero ())
else begin
let s = ref (O.zero ()) in
let rec forloop (i: int63) = (* for i = 0 to n-1 do *)
requires { 0 <= to_int i <= to_int n }
requires { is_board board (to_int pos) }
variant { to_int n - to_int i }
ensures { is_board board (to_int pos) }
if i < n then begin
board[pos] <- i;
if mcheck_is_consistent board pos then
s := O.add !s (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);
!s
end
let mcount_queens (board: array int63) (n: int63) : O.t
requires { to_int (length board) = to_int n }
ensures { true }
= mcount_bt_queens board n (of_int 0)
let test_mcount_8 () =
let n = of_int 8 in
let a = Array63.make n (of_int 0) in
mcount_queens a n
***)
end
examples/vstte10_queens/why3session.xml
View file @
312f137e
...
...
@@ -2,43 +2,149 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"C
oq
"
version=
"
8
.4
pl4
"
timelimit=
"
20
"
memlimit=
"0"
/>
<prover
id=
"0"
name=
"C
VC4
"
version=
"
1
.4"
timelimit=
"
6
"
memlimit=
"
100
0"
/>
<prover
id=
"1"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"20"
memlimit=
"0"
/>
<prover
id=
"2"
name=
"Alt-Ergo"
version=
"0.95.1"
timelimit=
"20"
memlimit=
"0"
/>
<prover
id=
"3"
name=
"Z3"
version=
"3.2"
timelimit=
"8"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"4"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"6"
memlimit=
"0"
/>
<prover
id=
"5"
name=
"Z3"
version=
"4.3.1"
timelimit=
"6"
memlimit=
"1000"
/>
<file
name=
"../vstte10_queens.mlw"
expanded=
"true"
>
<theory
name=
"NQueens"
sum=
"
762623aaf4b051407a7a7e388df720fc"
expanded=
"tru
e"
>
<goal
name=
"eq_board_set"
expanded=
"true"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.00"
/></proof>
<theory
name=
"NQueens"
sum=
"
05ca6b285c56c769408f7ad47741cff
e"
>
<goal
name=
"eq_board_set"
>
<proof
prover=
"4"
timelimit=
"5"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.00"
steps=
"7"
/></proof>
</goal>
<goal
name=
"eq_board_sym"
expanded=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<goal
name=
"eq_board_sym"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
steps=
"7"
/></proof>
</goal>
<goal
name=
"eq_board_trans"
expanded=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<goal
name=
"eq_board_trans"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
</goal>
<goal
name=
"eq_board_extension"
expanded=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<goal
name=
"eq_board_extension"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
steps=
"9"
/></proof>
</goal>
<goal
name=
"consistent_row_eq"
expanded=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.06"
/></proof>
<goal
name=
"consistent_row_eq"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.06"
steps=
"37"
/></proof>
</goal>
<goal
name=
"WP_parameter check_is_consistent"
expl=
"VC for check_is_consistent"
expanded=
"true"
>
<goal
name=
"WP_parameter check_is_consistent"
expl=
"VC for check_is_consistent"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"solution_eq_board"
expanded=
"true"
>
<proof
prover=
"0"
edited=
"vstte10_queens_NQueens_solution_eq_board_1.v"
><result
status=
"valid"
time=
"1.31"
/></proof>
<goal
name=
"solution_eq_board"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"WP_parameter bt_queens"
expl=
"VC for bt_queens"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"1.
46
"
/></proof>
<goal
name=
"WP_parameter bt_queens"
expl=
"VC for bt_queens"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"1.
21
"
/></proof>
</goal>
<goal
name=
"WP_parameter queens"
expl=
"VC for queens"
expanded=
"true"
>
<proof
prover=
"4"
timelimit=
"20"
><result
status=
"valid"
time=
"0.02"
/></proof>
<goal
name=
"WP_parameter queens"
expl=
"VC for queens"
>
<proof
prover=
"4"
timelimit=
"20"
><result
status=
"valid"
time=
"0.02"
steps=
"21"
/></proof>
</goal>
<goal
name=
"WP_parameter test8"
expl=
"VC for test8"
expanded=
"true"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
/></proof>
<goal
name=
"WP_parameter test8"
expl=
"VC for test8"
>
<proof
prover=
"4"
timelimit=
"5"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"0"
/></proof>
</goal>
<goal
name=
"WP_parameter count_bt_queens"
expl=
"VC for count_bt_queens"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"WP_parameter count_queens"
expl=
"VC for count_queens"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
</goal>
<goal
name=
"WP_parameter test_count_8"
expl=
"VC for test_count_8"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"0"
/></proof>
</goal>
</theory>
<theory
name=
"MachineArithmetic"
sum=
"0500018a9f9265efb1b389c414cb9813"
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. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.2"
expl=
"2. index in array bounds"
>
<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. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"17"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.4"
expl=
"4. precondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.5"
expl=
"5. integer overflow"
>
<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=
"1000"
><result
status=
"valid"
time=
"0.04"
steps=
"47"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.7"
expl=
"7. variant decrease"
>
<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.02"
steps=
"23"
/></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=
"23"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.10"
expl=
"10. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"23"
/></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=
"28"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.12"
expl=
"12. integer overflow"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.15"
steps=
"62"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.13"
expl=
"13. variant decrease"
>
<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=
"31"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.15"
expl=
"15. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.48"
steps=
"81"
/></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>
<goal
name=
"WP_parameter mcount_bt_queens.17"
expl=
"17. integer overflow"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"20"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.18"
expl=
"18. integer overflow"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.08"
steps=
"47"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.19"
expl=
"19. variant decrease"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"23"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.20"
expl=
"20. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"23"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.21"
expl=
"21. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.23"
steps=
"65"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.22"
expl=
"22. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"27"
/></proof>
</goal>
<goal
name=
"WP_parameter mcount_bt_queens.23"
expl=
"23. postcondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"15"
/></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>
<goal
name=
"WP_parameter mcount_bt_queens.25"
expl=
"25. precondition"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"12"
/></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=
"12"
/></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>
</transf>
</goal>
<goal
name=
"WP_parameter mcount_queens"
expl=
"VC for mcount_queens"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"14"
/></proof>
</goal>
<goal
name=
"WP_parameter test_mcount_8"
expl=
"VC for test_mcount_8"
>
<proof
prover=
"4"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
</theory>
</file>
...
...
examples/vstte10_queens/why3shapes.gz
View file @
312f137e
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