Next / Previous / Contents / Shipman's homepage

7.1. Trace table: SudokuSolver.__init__()

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:

  1. self.givenPuzzle is not a valid puzzle. See Section 7.1.1, “Case 1: Not a valid puzzle”.

  2. self.givenPuzzle is a valid puzzle. See Section 7.1.2, “Case 2: Valid puzzle”.

7.1.1. Case 1: Not a 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 ]

7.1.2. Case 2: Valid puzzle

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 ]