Guarded Commands, Nondeterminacy and Formal Derivation of Programs-英文文献.pdf

Programming T.A. Standish Languages Editor Guarded Commands, 1. Introduction Nondeterminacy and In Section 2, two statements, an alternative con- struct and a repetitive construct, are introduced, to- Formal Derivation gether with an intuitive (mechanistic) definition of their semantics. The basic building block for both of them of Programs is the so-called guarded command, a statement list prefixed by a boolean expression: only when this boolean expression is initially true, is the statement list Edsger W. Dijkstra eligible for execution. The potential nondeterminacy Burroughs Corporation allows us to map otherwise (trivially) different programs on the same program text, a circumstance that seems largely responsible for the fact that programs can now be derived in a manner more systematic than before. In Section 3, after