article

Free access

Guarded commands, nondeterminacy and formal derivation of programs

Author:

Edsger W. DijkstraAuthors Info & Claims

Communications of the ACM, Volume 18, Issue 8

Pages 453 - 457

https://doi.org/10.1145/360933.360975

Published: 01 August 1975 Publication History

PDF eReader

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.

References

[1]

Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), 576-583.

Digital Library

Google Scholar

[2]

Naur, Peter (Ed.). Report on the algorithmic language ALGOL 60. Comm. ACM 3, (May 1960), 299-314.

Digital Library

Google Scholar

Cited By

View all

Platzer A(2025)Hybrid dynamical systems logic and its refinementsScience of Computer Programming10.1016/j.scico.2024.103179239(103179)Online publication date: Jan-2025
https://doi.org/10.1016/j.scico.2024.103179
Campbell EHojjat HFoster N(2024)Computing Precise Control Interface SpecificationsProceedings of the ACM on Programming Languages10.1145/36897438:OOPSLA2(905-934)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689743
Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689740
Show More Cited By

Index Terms

Guarded commands, nondeterminacy and formal derivation of programs
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
    2. General programming languages
      1. Language types
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation

Recommendations

Guarded commands, non-determinacy and a calculus for the derivation of programs
Proceedings of the international conference on Reliable software

So-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 Software

So-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

Information & Contributors

Information

Published In

Communications of the ACM Volume 18, Issue 8

Aug. 1975

52 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/360933

Editor:
Robert L. Ashenhurst
Univ. of Chicago, Chicago, IL

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1975

Published in CACM Volume 18, Issue 8

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1,648
Total Citations
View Citations
6,088
Total Downloads

Downloads (Last 12 months)683
Downloads (Last 6 weeks)83

Reflects downloads up to 21 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Platzer A(2025)Hybrid dynamical systems logic and its refinementsScience of Computer Programming10.1016/j.scico.2024.103179239(103179)Online publication date: Jan-2025
https://doi.org/10.1016/j.scico.2024.103179
Campbell EHojjat HFoster N(2024)Computing Precise Control Interface SpecificationsProceedings of the ACM on Programming Languages10.1145/36897438:OOPSLA2(905-934)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689743
Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689740
Frölich Dvan Binsbergen LChiba SThüm T(2024)On the Soundness of Auto-completion Services for Dynamically Typed LanguagesProceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690734(107-120)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690734
Kura SUnno H(2024)Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type SystemProceedings of the ACM on Programming Languages10.1145/36746628:ICFP(973-1002)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674662
Barrett CCastle DHeijltjes WSobocinski PLago UEsparza J(2024)The Relational Machine CalculusProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662091(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662091
Spies SGäher LSammler MDreyer D(2024)Quiver: Guided Abductive Inference of Separation Logic Specifications in CoqProceedings of the ACM on Programming Languages10.1145/36564138:PLDI(889-913)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656413
Zilberstein NSaliling ASilva A(2024)Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational EffectsProceedings of the ACM on Programming Languages10.1145/36498218:OOPSLA1(276-304)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649821
Din CHähnle RHenrio LJohnsen EPun VTarifa S(2024)Locally Abstract, Globally Concrete Semantics of Concurrent Programming LanguagesACM Transactions on Programming Languages and Systems10.1145/364843946:1(1-58)Online publication date: 16-Feb-2024
https://dl.acm.org/doi/10.1145/3648439
Qin XO’Connor Lvan Glabbeek RHöfner PKammar OSteuwer M(2024)Shoggoth: A Formal Foundation for Strategic RewritingProceedings of the ACM on Programming Languages10.1145/36332118:POPL(61-89)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633211
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Guarded commands, non-determinacy and a calculus for the derivation of programs

Guarded commands, non-determinacy and a calculus for the derivation of programs

An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations