Edsger W. Dijkstra introduced guarded commands as a building block for alternative and repetitive constructs, allowing for nondeterministic program components. These constructs enable programs to have multiple possible outcomes, with the final state not necessarily uniquely determined by the initial state. A formal calculus for deriving programs using these constructs is presented, emphasizing the use of weakest preconditions to ensure correctness. The alternative construct is defined using "if" and "fi" to select between guarded lists based on boolean conditions. The repetitive construct uses "do" and "od" to repeatedly execute guarded lists until all guards are false. Both constructs allow for nondeterminacy, where multiple execution paths are possible. The formal semantics of these constructs are defined using predicate transformers, which associate preconditions with postconditions. The weakest precondition (wp) is used to determine the initial state required for a program to terminate correctly. Theorems are derived to show how these constructs can be used to derive correct programs. The article illustrates the use of guarded commands in deriving programs for tasks such as finding the maximum of two values and computing the greatest common divisor (gcd). The formal derivation process involves selecting an invariant relation and a variant function to ensure the program's correctness. Dijkstra emphasizes the importance of formal methods in programming, particularly the use of predicate transformers to define program semantics. He contrasts this approach with traditional programming methods, highlighting the benefits of a systematic, formal derivation process. The article concludes with acknowledgments to colleagues and the significance of nondeterminacy in programming, noting its potential for both correctness and efficiency.Edsger W. Dijkstra introduced guarded commands as a building block for alternative and repetitive constructs, allowing for nondeterministic program components. These constructs enable programs to have multiple possible outcomes, with the final state not necessarily uniquely determined by the initial state. A formal calculus for deriving programs using these constructs is presented, emphasizing the use of weakest preconditions to ensure correctness. The alternative construct is defined using "if" and "fi" to select between guarded lists based on boolean conditions. The repetitive construct uses "do" and "od" to repeatedly execute guarded lists until all guards are false. Both constructs allow for nondeterminacy, where multiple execution paths are possible. The formal semantics of these constructs are defined using predicate transformers, which associate preconditions with postconditions. The weakest precondition (wp) is used to determine the initial state required for a program to terminate correctly. Theorems are derived to show how these constructs can be used to derive correct programs. The article illustrates the use of guarded commands in deriving programs for tasks such as finding the maximum of two values and computing the greatest common divisor (gcd). The formal derivation process involves selecting an invariant relation and a variant function to ensure the program's correctness. Dijkstra emphasizes the importance of formal methods in programming, particularly the use of predicate transformers to define program semantics. He contrasts this approach with traditional programming methods, highlighting the benefits of a systematic, formal derivation process. The article concludes with acknowledgments to colleagues and the significance of nondeterminacy in programming, noting its potential for both correctness and efficiency.