The article introduces "guarded commands" as a fundamental building block for constructing alternative and repetitive constructs in programming languages, allowing for nondeterministic behavior. These constructs enable programs to be derived formally, ensuring correctness and termination. The authors define the semantics of these constructs using predicate transformers and present a formal calculus for program derivation. They illustrate the use of these constructs with examples, including finding the maximum of two values and computing the greatest common divisor of two numbers. The article emphasizes the importance of invariant relations and variant functions in the derivation process. The authors also discuss the advantages of using guarded commands over traditional constructs, highlighting their simplicity and elegance. The research is motivated by the need to understand and formalize programming activities, particularly the creation of invariant relations and variant functions. The article concludes with reflections on the potential nondeterminacy in programs and its implications for hardware and software reliability.The article introduces "guarded commands" as a fundamental building block for constructing alternative and repetitive constructs in programming languages, allowing for nondeterministic behavior. These constructs enable programs to be derived formally, ensuring correctness and termination. The authors define the semantics of these constructs using predicate transformers and present a formal calculus for program derivation. They illustrate the use of these constructs with examples, including finding the maximum of two values and computing the greatest common divisor of two numbers. The article emphasizes the importance of invariant relations and variant functions in the derivation process. The authors also discuss the advantages of using guarded commands over traditional constructs, highlighting their simplicity and elegance. The research is motivated by the need to understand and formalize programming activities, particularly the creation of invariant relations and variant functions. The article concludes with reflections on the potential nondeterminacy in programs and its implications for hardware and software reliability.