A sudoku solver |  |
A sudoku solver | |
One important technique from the Cleanroom methodology is the use of trace tables to assist the verification panel in the inspection of the code.
For some simpler modules, there is a single sequence of trace tables that traces the state changes through that module. For each numbered prime (primary program refinement) of the module, we display first the intended function for that prime, followed by a table showing the values of all state items whose state has changed. The final set of state changes should match the overall intended function of the module.
In general, however, there are multiple trace table sequences for different cases of the logic. In that case, the trace table exposition for that module starts out with a list of all the cases. For each case, there is a trace table sequence showing the state changes in that case.
In the trace table for the constructor, the final
state should show that all invariants are true.
For the code, see Section 5.4, “SudokuSolver.__init__():
Constructor”.
Here are the cases:
self.givenPuzzle is not a
valid puzzle. See Section 7.1.1, “Case 1: Not a valid puzzle”.
self.givenPuzzle is a
valid puzzle. See Section 7.1.2, “Case 2: Valid puzzle”.
In prime 1 of this constructor, the actual code serves as the intended function.
#-- 1 --
self.givenPuzzle = givenPuzzle
self.solutionObserver = solutionObserver
self.changeObserver = changeObserver
self.nStateChanges = 0
self.nSolutions = 0
self.givenPuzzle
|
givenPuzzle as passed to constructor
|
self.solutionObserver
|
solutionObserver as passed to constructor
|
self.changeObserver
|
changeObserver as passed to constructor
|
self.nStateChanges
|
0
|
self.nSolutions
|
0
|
#-- 2 --
# [ self.givenPuzzle is a string ->
# if self.givenPuzzle is a valid sudoku puzzle as a string ->
# self.__board := a list of BOARD_L integers
# representing that puzzle
# else -> raise ValueError ]
By case assumption, self.givenPuzzle is not a valid puzzle,
so the next state change is to raise ValueError.
Here is the overall intended function:
[ (givenPuzzle is a sudoku puzzle as a string) and
(solutionObserver is a procedure or None) and
(changeObserver is a procedure or None) ->
if givenPuzzle is a valid sudoku puzzle ->
...
else ->
raise ValueError ]
The case assumption here is that the givenPuzzle string is a valid puzzle.
#-- 1 --
self.givenPuzzle = givenPuzzle
self.solutionObserver = solutionObserver
self.changeObserver = changeObserver
self.nStateChanges = 0
self.nSolutions = 0
self.givenPuzzle
|
givenPuzzle as passed to constructor
|
self.solutionObserver
|
solutionObserver as passed to constructor
|
self.changeObserver
|
changeObserver as passed to constructor
|
self.nStateChanges
|
0
|
self.nSolutions
|
0
|
#-- 2 --
# [ self.givenPuzzle is a string ->
# if self.givenPuzzle is a valid sudoku puzzle as a string ->
# self.__board := a list of BOARD_L integers
# representing that puzzle
# else -> raise ValueError ]
self.givenPuzzle
|
givenPuzzle as passed to constructor
|
self.solutionObserver
|
solutionObserver as passed to constructor
|
self.changeObserver
|
changeObserver as passed to constructor
|
self.nStateChanges
|
0
|
self.nSolutions
|
0
|
self.__board
|
a list of BOARD_L
integers representing self.givenPuzzle
|
#-- 3 --
# [ self.__given := a copy of self.__board ]
self.givenPuzzle
|
givenPuzzle as passed to constructor
|
self.solutionObserver
|
solutionObserver as passed to constructor
|
self.changeObserver
|
changeObserver as passed to constructor
|
self.nStateChanges
|
0
|
self.nSolutions
|
0
|
self.__board
|
a list of BOARD_L
integers representing self.givenPuzzle
|
self.__given
|
a list of BOARD_L
integers representing self.givenPuzzle
|
Compare the states above with the class invariants:
Exports:
.givenPuzzle: [ as passed to constructor, read-only ]
.solutionObserver: [ as passed to constructor, read-only ]
.changeObserver: [ as passed to constructor, read-only ]
State/Invariants:
.nStateChanges: [ number of cell state changes so far ]
.nSolutions: [ number of solutions seen so far ]
.__given:
[ the initial state of the puzzle as a list of integers ]
.__board:
[ the current state of the puzzle as a list of integers ]