N Queens

July 1, 2012 – 4 years, 8 months ago, by vladimir

Short Description

Write/verify a program to place N queens on an N×N chess board so that no queen can capture another one with a legal move.

Code

In the following sample code, the search for a consistent board position is defined recursively over the columns (pos) and scanning each position for a row value (i).

def Search(int pos, int[] board) : int[] {
  if (pos == board.length) {
    return board;
  }

  for (int i = 0; i < board.length; i++) {
    board[pos] = i;

    if (IsConsistent(board, pos)) {
      int[] s = Search(pos + 1, board);

      if (s != null) {
        return s;
      }
    }
  }

  return null;
}

def IsConsistent(int[] board, int pos) : boolean {
  for (int q = 0; q < pos; q++) {
    if ((board[q] == board[pos]) || 
         (board[q] - board[pos] == pos - q)||
         (board[pos] - board[q] == pos - q)) {
      return false;
    }
  }
  return true;
}

Specification

The post-condition should establish that when the algorithm returns a placement, it is legal, and if it returns an empty board, there is no solution.

A legal board is defined by the operation IsConsistent.

Long Description

The algorithm should return a placement if there is a solution, and an empty board, otherwise. You can represent the empty board with a flag or a null pointer.

A placement is given by a board which is an N-element array where the i'th element is j, when the queen is placed in the j'th row of the i'th column.

Supplementary Materials

With N=2, the result should be empty, whereas with N=4, there should be a legal placement.

This problem was posed at the VSTTE'10 verification competition by Peter Müller <Peter.Mueller@inf.ethz.ch> and Natarajan Shankar <shankar@csl.sri.com>.

If you want to attach a file, please attach to this page and post a link here.

Submitted by

Vladimir Klebanov <verifythis@cost-ic0701.org>


Solution

Tool/Method

Holfoot

Code/Specification

The progam is written in Holfoot's imperative programming language. The specification heavily relies on predicates that are defined in
the interactive proof script.

val IS_CONSISTENT_BOARD_REC_def = Define `
  IS_CONSISTENT_BOARD_REC (n:num) (p:num) l =
  !q. q < n ==>
     (~(EL q l = EL p l) /\
      ~((EL q l - EL p l) = (p - q)) /\
      ~((EL p l - EL q l) = (p - q)))`;

val IS_CONSISTENT_BOARD_def = Define `
  IS_CONSISTENT_BOARD l =
  ((!p. p < (LENGTH l) ==> IS_CONSISTENT_BOARD_REC p p l) /\
  (EVERY (\x. x < LENGTH l) l))`;

IS_CONSISTENT_BOARD_REC captures the semantics of the IsConsistent procedure. In order to use it for the loop specification as well, an extra parameter (q) has been added. IS_CONSISTENT_BOARD then captures the desired overall goal. It's definition is in terms of IS_CONSISTENT_BOARD_REC. This makes the program easier to prove. To show, that it really has the intended meaning, the following lemma is proved:

val IS_CONSISTENT_BOARD___REWRITE = prove (
``IS_CONSISTENT_BOARD l =
  ((EVERY (\x. x < LENGTH l) l) /\
   (!i1 i2. (i1 < i2 /\ i2 < (LENGTH l)) ==>
        (~(EL i1 l = EL i2 l) /\
         ~((EL i1 l - EL i2 l) = (i2 - i1)) /\
         ~((EL i2 l - EL i1 l) = (i2 - i1)))))``,
...

Solution-problem relationship

Holfoot supports just a tiny subset of C. This subset is, however, formalised in the HOL 4 theorem prover and after parsing, all verification steps are done by proof inside HOL 4. Some syntax used in the pseudo code is not available. Thus, the for-loop has been replaced by a while-loop. Furthermore, the syntax "board[pos]" is not available for arrays. Instead "(board + pos)->dta" is used. Moreover, local variables are introduced to hold the values of array values, because Holfoot requires heap lookups to be separate instructions. Most annoying is, that Holfoot does not support "return". Therefore, an extra call by reference argument "r" is added to the procedures and used as a return argument. The return statement can't terminate the execution of the loop, though. Therefore, this argument doubles as a flag to exit the loop early.

Since search is calling itself recursively, it's specification has to take care of recursive calls. In order to get a clean / user level interface, an extra function

find
was added that has a cleaner, high level specification.

Interactivity, effort needed

Verifying this program took considerable interactive effort. I had trouble getting the specification right. It took me a moment to get the loop-invariant for the loop in search. One I had the loop specification, it was easy to prove using Holfoot. The interactive proof script is lengthy, but easy. Altogether it took me about 3 hours.

How to reproduce

The example is available with Holfoot. It is easiest to use the Webinterface to run the example. However, one can download the sources and run the example inside HOL 4 as well.

Published

Submitted by

Thomas Tuerk


Solution

Author

K. Rustan M. Leino

Tool/Method

Dafny

Code/Specification

Dafny is an object-based language with built-in specification constructs.
To a first approximation, it is like Java (but without subclasses) with Eiffel- or JML-like specifications. Language features that are especially useful when writing specifications include sets and sequences, ghost variables, and user-defined recursive functions.
Dafny uses mathematical integers (implemented by big-nums), which avoids overflow errors.

Solution-problem relationship

Interactivity, effort needed

The problem was solved for the experience report in the aftermath of the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes a file "VSComp-Leino-4.dfy" which can be run with the Dafny tool.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)


Solution

Author

Bart Jacobs, Frank Piessens and Jan Smans

Tool/Method

VeriFast
VeriFast is a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.

Code/Specification

This program employs the standard Valid()/Repr idiom used in the dynamic-frames
style of specifications. Within that idiom, the specification is straightforward (if verbose), and there are no particular wrinkles or annoyances in getting the verifier to prove the correctness.

Solution-problem relationship

Interactivity, effort needed

The problem was solved for the experience report in the aftermath of the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes a file "NQueens.java" which can be run with the tool.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)


Solution

Author

Vladimir Klebanov, Mattias Ulbrich and Benjamin Weiß

Tool/Method

KeY. An automated/interactive tool for Java source code verification using dynamic logic.
A developer version was used, which contains bugfixes that will be part of the upcoming 1.6 release. In the meantime, the particular version can be accessed via web start here.

Code/Specification

Straight-forward JML specification.

Solution-problem relationship

The correctness of this program relies on some properties of Queens boards. These
are stated and proved as lemmas, which here are given in assert statements.

Interactivity, effort needed

The problem was solved for the experience report in the aftermath of the VSTTE'10 competition.
All three proof obligations can be verified without user interaction.

How to reproduce

You can load the evidence file "Queens_search.proof" into the web start version of KeY linked above. This will provide you with a complete proof script in dynamic logic.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)