Hoare Logic

Rules

Assignment rule

$\par\frac{}{\Hoare{{P}[E/x]}{x:=E}{P}}$

If rule

$\par\frac{\Hoare{P\land\llbracket{b}\rrbracket}{c_{1}}{Q}\qquad\Hoare{P\land% \lnot\llbracket{b}\rrbracket}{c_{2}}{Q}}{\Hoare{P}{\mathsf{if}\;b\;\mathsf{% then}\;c_{1}\mathsf{else}\;c_{2}}{Q}}$

While Rule

The Partial Correctness rule for while loops is the following, where $\phi$ is the loop invariant.

$\par\frac{P\Rightarrow\phi\qquad\Hoare{\phi\land\llbracket{e}\rrbracket}{c}{% \phi}\qquad{\phi\land\lnot\llbracket{e}\rrbracket}\Rightarrow{Q}}{\Hoare{P}{% \mathsf{while}\;e\;\mathsf{do}\;c}{Q}}$

For total correctness, we need to add a variant alongside our loop invariant; this is some Well-Founded Relation that we need to ensure strictly decreases on every iteration, and also add conditions that ensure that evaluating the loop body and loop guard dont crash.