I was enjoying "The Humble Programmer" earlier today and ran across this choice quote:

Therefore, for the time being and perhaps forever, the rules of the second kind present themselves as elements of discipline required from the programmer. Some of the rules I have in mind are so clear that they can be taught and that there never needs to be an argument as to whether a given program violates them or not. Examples are the requirements that no loop should be written down without providing a proof for termination nor without stating the relation whose invariance will not be destroyed by the execution of the repeatable statement.

I'm looking for which of Dijkstra's 1300+ writings best describe in further detail rules such as he was describing above.