69 lines
1.4 KiB
Text
69 lines
1.4 KiB
Text
int abs(i: int) {
|
|
if (i >= 0) return i; else return -i;
|
|
}
|
|
|
|
unit print_dots(n: int) {
|
|
while (n > 0) { print_string("."); n = n - 1; }
|
|
return;
|
|
}
|
|
|
|
{size:int | 0 < size}
|
|
unit print_board (board[size]: int, size: int(size)) {
|
|
var: int n, row;;
|
|
|
|
invariant: [i:nat] (row: int(i))
|
|
for (row = 0; row < size; row = row + 1) {
|
|
n = board[row];
|
|
print_dots(n-1);
|
|
print_string("Q");
|
|
print_dots(size - n);
|
|
print_newline();
|
|
}
|
|
print_newline();
|
|
return;
|
|
}
|
|
|
|
{size:int, j:int | 0 <= j < size}
|
|
bool test (j: int(j), board[size]: int) {
|
|
var: int diff, i, qi, qj;;
|
|
|
|
qj = board[j];
|
|
|
|
invariant: [i:nat] (i: int(i))
|
|
for (i = 0; i < j; i = i + 1) {
|
|
qi = board[i]; diff = abs (qi - qj);
|
|
if (diff == 0) { return false; }
|
|
else { if (diff == j - i) return false; }
|
|
}
|
|
return true;
|
|
}
|
|
|
|
{size:int | 0 < size}
|
|
nat queen(size: int(size)) {
|
|
var: int board[], next, row; nat count;;
|
|
|
|
count = 0; row = 0; board = alloc(size, 0);
|
|
|
|
invariant: [n:nat | n < size] (row: int(n))
|
|
while (true) {
|
|
next = board[row]; next = next + 1;
|
|
if (next > size) {
|
|
if (row == 0) break; else { board[row] = 0; row = row - 1; }
|
|
} else {
|
|
board[row] = next;
|
|
if (test(row, board)) {
|
|
row = row + 1;
|
|
if (row == size) {
|
|
count = count + 1;
|
|
print_board(board, size);
|
|
row = row - 1;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
return count;
|
|
}
|
|
|
|
int main () {
|
|
return queen (8);
|
|
}
|