Oops!! Earlier, I replied:
+---------------
| Anyway, sorry for the sledghammer overkill, but I cannot stress
| enough that in the Dijkstra/Gries formalism one is *never*
| "proving the code"; instead, the proof *writes* the code.
| 
| Of course, that doesn't relieve the fact that *finding* the proof
| [especially in the case of loops] is not the hard part...  ;-}
+---------------

Of course that final "not" was a typo; it *should* have read:

  Of course, that doesn't relieve the fact that *finding* the proof
  [especially in the case of loops] is the hard part...
				   ****

-Rob

-----
Rob Warnock			<rpw3@rpw3.org>
627 26th Avenue			<URL:http://rpw3.org/>
San Mateo, CA 94403		(650)572-2607