Algorithm Development and Correctness

Long ago I gave a course for M.Sc. students on program correctness, sharing it in some years with Joseph Goguen. My notes for that course still exist somewhere, and it would be nice to find them and put them here. Among other things, they contain a careful treatment of the semantics of Dijkstra's guarded command language that defines the weakest precondition of a loop as the strongest solution of a certain fixed-point equation.

For those who wonder what it was like to teach a course with Joseph: nothing that I might say can express it better than this poem, Zero, Connected, Empty, written by him.