S

#### Stefan Ram

Jim Janney said:while (x < 20)

(...)

/* postcondition: x >= 20 (from the condition of the while) */

I even read once that some people prefer »while( x != 21 )«

for such loops so as to get a more precise postcondition »x == 20«.

From the point of view of »defensive programming« OTOH, »x <

20« can avoid an endless loop (in case of bugs) better than

»x != 21«.

Even in mathematics, proofs do not have to be »formal«.

They need to convey that an assertion is true beyond any

reasonable doubt to a sufficiently educated reader.