Formally, a program (or more accurately, an executable fragment or small module) is given by its state-space, a precondition, and a postcondition. The guarded command language gives us a way to reason about such programs or executable fragments of code--a set of inference rules is given that show how to prove that a certain statement S satisfies a given specification. Such proofs are important tools for verification.

The basic structure of a claim in the formal specification of a program fragment is {P} S {Q} where P is the precondition and Q is the postcondition; the statement simply means, "Each execution of S terminates in a state satisfying Q, when applied to a state satisfying P."

Based on simple rules of propositional logic, a few observations can be made. For instance, {P} S {false} denotes a program segment S that always produces false, i...