Laws of programming
C. A. R. Hoare, Ian J. Hayes, He Jifeng, Carroll C. Morgan, Andrew William Roscoe, Jeff W. Sanders, Ib Holm Sørensen, Justin M Spivey, Bernard Sufrin · Communications of the ACM · 1987
A complete set of algebraic laws is given for Dijkstra's nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott's domain theory as fixed points of continuous functionals. A calculus analogous to weakest preconditions is suggested as an aid to deriving programs from their specifications.