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);
}