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 ($\Pi ;\Omega$). It is defined as:

$$\frac{\{F\}\Pi \{G\}\{G\}\Omega \{H\}}{\{F\}\Pi ;\Omega \{H\}}{}_{\text{(comp)}}$$

Reasoning

To prove that the sequence $\Pi ;\Omega$ satisfies the specification $(F,H)$, one must find an intermediate assertion $G$ such that:

1. $\Pi$ starts in $F$ and ends in $G$.
2. $\Omega$ starts in $G$ and ends in $H$.

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

Associativity

Sequential composition is associative. Proving $\{F\}\Pi ;\Omega ;\Psi \{H\}$ involves finding two intermediate assertions.