7.3. Trace table: SudokuSolver.get()

7.3. Trace table: `SudokuSolver.get()`

Cases:

The row index x is not in the interval [0,MAT_L). See Section 7.3.1, “Case 1: Row index out of range”.
The row index x is in [0,MAT_L) but the column index yis not in [0,MAT_L). See Section 7.3.2, “Case 2: Valid row index, invalid column index”.
The row and column indices are both valid. See Section 7.3.3, “Case 3: Valid row and column indices”.

7.3.1. `Case 1: Row index out of range`

The case assumption is that the row index r is not in the interval [0,MAT_L), that is, it is not a valid row index.

        #-- 1 --
        if  not ( 0 <= r < MAT_L ):
            raise KeyError, ( "SudokuSolver.get(): Bad row "
                "index, %d." % r )

This raises KeyError, satisfying the goal state:

          [ r and c are integers ->
              if (0<=r<MAT_L) and (0<=r<MAT_L) ->
                ...
              else -> raise KeyError

7.3.2. Case 2: Valid row index, invalid column index

The case assumption here is that r is in the interval [0,MAT_L) but c is not.

        #-- 1 --
        # [ if r is in [0,MAT_L) ->
        #     I
        #   else -> raise KeyError ]

By case assumption, this does nothing (the identity transform “I”).

        #-- 2 --
        # [ if c is in [0,MAT_L) ->
        #     I
        #   else -> raise KeyError ]

This raises KeyError, satisfying the goal state:

          [ r and c are integers ->
              if (0<=r<MAT_L) and (0<=r<MAT_L) ->
                ...
              else -> raise KeyError

7.3.3. Case 3: Valid row and column indices

The case assumption here is that both r and c fall in the interval [0,MAT_L).

        #-- 1 --
        # [ if r is in [0,MAT_L) ->
        #     I
        #   else -> raise KeyError ]

Does nothing.

        #-- 2 --
        # [ if c is in [0,MAT_L) ->
        #     I
        #   else -> raise KeyError ]

Does nothing.

        #-- 3 --
        # [ x  :=  index in self.__board corresponding to row r,
        #          column c ]

x Index in self.__board corresponding to row r, column c

        #-- 4 --
        return  self.__board[x]

This returns the element of self.__board corresponding to row r and column c, satisfying the goal state:

          [ r and c are integers ->
              if (0<=r<MAT_L) and (0<=c<MAT_L) ->
                return the state of the cell at row r and column c
                as 0 for empty, or an integer in [1,9] if set
              else -> ... ]

Note the invariant on self.__board has matching verbiage:

        .__board:
          [ the current state of the puzzle as a list of integers,
            0 for empty, or in [1,9] if set ]

A sudoku solver