Hoare logic

Definition

Consider the while language, whose commands are $C ::= \mathsf{skip} \mid x := E \mid C; C \mid \mathsf{if}\ B\ \mathsf{then}\ C\ \mathsf{else}\ C \mid \mathsf{while}\ B\ \mathsf{do}\ C$, where $E$ ranges over integer expressions and $B$ over boolean expressions in the program variables. Assertions $P, Q, R$ are formulas of first-order predicate logic over the integers whose free variables may include the program variables. A Hoare triple is an expression $\set{P}\, C\, \set{Q}$. Runs of commands are given by the operational semantics of the language. The triple is valid if, for every state $s$ satisfying $P$, every terminating run of $C$ from $s$ ends in a state satisfying $Q$. Hoare logic is the proof system whose derivable triples are generated by these rules.

1. Skip: $\set{P}\, \mathsf{skip}\, \set{P}$.
2. Assignment: $\set{Q[E/x]}\, x := E\, \set{Q}$, where $Q[E/x]$ is the substitution of $E$ for $x$ in $Q$.
3. Composition: from $\set{P}\, C_1\, \set{R}$ and $\set{R}\, C_2\, \set{Q}$ derive $\set{P}\, C_1; C_2\, \set{Q}$.
4. Conditional: from $\set{P \land B}\, C_1\, \set{Q}$ and $\set{P \land \lnot B}\, C_2\, \set{Q}$ derive $\set{P}\, \mathsf{if}\ B\ \mathsf{then}\ C_1\ \mathsf{else}\ C_2\, \set{Q}$.
5. While: from $\set{I \land B}\, C\, \set{I}$ derive $\set{I}\, \mathsf{while}\ B\ \mathsf{do}\ C\, \set{I \land \lnot B}$.
6. Consequence: from $P \Rightarrow P'$, $\set{P'}\, C\, \set{Q'}$ and $Q' \Rightarrow Q$, where the implications are true in the integers, derive $\set{P}\, C\, \set{Q}$.