A sudoku solver

Verification of this method is aided by the vague wording of its intended function:

          [ outFile is a writeable file ->
              outFile  +:=  a representation of self's state in
                  input-file format ]

The output format here is pretty simple, and assumes that it will be viewed in a monospaced font. Each row is written with a space between columns, with two extra spaces added between columns 2 and 3 and again between columns 5 and 6. We also print a blank line between rows 2 and 3, and again between rows 5 and 6. Here's a sample output:

7 2 .   . . 5   1 . .
. 1 5   9 8 .   4 . .
. 8 .   . . 1   . . 6

. 4 .   . 3 .   6 . 5
3 . .   6 . 2   . . 7
9 . 1   . 7 .   . 2 .

5 . .   7 . .   . 9 .
. . 2   . 9 6   3 5 .
. . 4   2 . .   . 6 8

Note the symmetry of the row and column presentation. We'll discuss the way it's implemented for the blank lines between rows; the same logic works for the extra spaces between columns.

We can test for the extra blank line either before writing each row of data, or after. It's pretty arbitrary, so we choose to test before writing the data. Below is a truth table for when to write the blank line. The author added a column for the index's remainder modulo SUBMAT_L. Why did the author do this? Well, when a behavior repeats cyclically, it suggests to the author that a modulo function is involved.

This table suggests that we could write the extra blank line whenever the row % SUBMAT_L is zero, but this logic would write an extra blank line initially. Therefore, the correct logic is: write an extra blank line before every row r for which ((r>0) and ((r % SUBMAT_L)==0). Here is the actual code:

        #-- 1 --
        for  rowx in range(MAT_L):
            #-- 1 body --
            # [ rowx is in [0,MAT_L) ->
            #     outFile  +:=  a representation of row rowx of self ]

            #-- 1.1 --
            # [ if ( ( rowx > 0 ) and
            #        ( rowx % SUBMAT_L ) == 0 ) ) ->
            #     outFile  +:=  an empty line
            #   else -> I ]
            if  ( ( rowx > 0 ) and
                  ( ( rowx % SUBMAT_L ) == 0 ) ):
                print >> outFile

            #-- 1.2 --
            # [ outFile  +:=  a representation of row rowx of self ]
            self.writeRow ( outFile, rowx )