Edsger W. Dijkstra
Abstract
So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be be shown.
- 1 Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), 576-583. Google Scholar
Digital Library
- 2 Naur, Peter (Ed.). Report on the algorithmic language ALGOL 60. Comm. ACM 3, (May 1960), 299-314. Google ScholarDigital Library
Index Terms
- Guarded commands, nondeterminacy and formal derivation of programs
Recommendations
Guarded commands, non-determinacy and a calculus for the derivation of programs
Proceedings of the international conference on Reliable softwareSo-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow non-deterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily ...
Guarded commands, non-determinacy and a calculus for the derivation of programs
International Conference on Reliable SoftwareSo-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow non-deterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily ...
An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs
The ideas behind correctness proofs for programs are outlined, and conventional definitions of assignment, etc., are given. The main part of this paper is the idealized development of a nontrivial program in a disciplined fashion. The use of Dijkstra's "...
Comments