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.

`row` | extra line? | `row % SUBMAT_L` |
---|---|---|

0 | 0 | 0 |

1 | 0 | 1 |

2 | 0 | 2 |

3 | 1 | 0 |

4 | 0 | 1 |

5 | 0 | 2 |

6 | 1 | 0 |

7 | 0 | 1 |

8 | 0 | 2 |

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 )