A sudoku solver

The case assumption is that the number of non-whitespace characters in self.givenPuzzle is not BOARD_L.

        #-- 1 --
        # [ charList  :=  a list whose elements are the
        #       non-whitespace characters of self.givenPuzzle in
        #       the same order ]

        #-- 2 --
        if  len(charList) != BOARD_L:
            raise ValueError, ( "Puzzle has %d nonblank "
                "characters; it should have exactly %d." %
                (len(charList), BOARD_L) )

By case assumption, the length of charList is not BOARD_L, so we raise ValueError. The overall intended function:

          [ self.givenPuzzle is a string ->
              if self.givenPuzzle is a sudoku puzzle ->
                ...
              else -> raise ValueError ]

The case assumptions are: self.givenPuzzle contains exactly BOARD_L non-whitespace characters, but at least one of those characters is not a digit or ".".

        #-- 1 --
        # [ charList  :=  a list whose elements are the
        #       non-whitespace characters of self.givenPuzzle in
        #       the same order ]

        #-- 2 --
        if  len(charList) != BOARD_L:
            raise ValueError, ( "Puzzle has %d nonblank "
                "characters; it should have exactly %d." %
                (len(charList), BOARD_L) )

By case assumption, the number of non-whitespace characters is exactly BOARD_L, so we proceed to the next prime. The trace table is unchanged.

        #-- 3 --
        # [ if each element of charList is either "." or in
        #   the interval ["1", "9"] ->
        #     result  :=  a list of integers corresponding to the
        #                 elements of charList consisting of
        #                 integer 0 where the value is "." and
        #                 int(c) for other values
        #   else ->
        #     raise ValueError ]

By case assumption, at least one non-whitespace character of self.givenPuzzle is neither a digit nor ".", so we raise ValueError. Here is the overall intended function:

          [ self.givenPuzzle is a string ->
              if self.givenPuzzle is a valid sudoku puzzle ->
                ...
              else -> raise ValueError ]

Case assumptions: the number of non-whitespace characters in self.givenPuzzle is exactly BOARD_L; and each of those characters is either a digit or ".".

        #-- 1 --
        # [ charList  :=  a list whose elements are the
        #       non-whitespace characters of self.givenPuzzle in
        #       the same order ]

        #-- 2 --
        if  len(charList) != BOARD_L:
            raise ValueError, ( "Puzzle has %d nonblank "
                "characters; it should have exactly %d." %
                (len(charList), BOARD_L) )

By case assumption, the number of non-whitespace characters is exactly BOARD_L, so we proceed to the next prime. The trace table is unchanged.

        #-- 3 --
        # [ if each element of charList is either "." or in
        #   the interval ["1", "9"] ->
        #     result  :=  a list of integers corresponding to the
        #         elements of charList consisting of integer 0
        #         where the value is "." and an integer in [1,9]
        #         where the value is a digit
        #   else ->
        #     raise ValueError ]

        #-- 4 --
        return result

This returns a list of values, each 0 if the corresponding non-whitespace character of self.givenPuzzle is ".", or an integer in [1,9] if the corresponding non-whitespace character of self.givenPuzzle is a digit. Compare this to the overall intended function:

          [ self.givenPuzzle is a string ->
              if self.givenPuzzle is a sudoku puzzle ->
                self.__board  :=  a list of BOARD_L integers
                                  representing that puzzle
              else -> ... ]