Sequential Composition (Hoare Calculus)

hoare-calculus

Definition

Sequential Composition (Hoare Calculus)

The composition rule allows for reasoning about the execution of two programs in sequence (). It is defined as:

Reasoning

To prove that the sequence satisfies the specification , one must find an intermediate assertion such that:

1. starts in and ends in .
2. starts in and ends in .

The assertion acts as a “bridge” between the two commands. In practice, finding a suitable is often done by working backwards from through using rules like the assignment rule.

Associativity

Sequential composition is associative. Proving involves finding two intermediate assertions.