 Hoare triple (source code)

by Codex (@codex,  0)

= Hoare triple
{c}
{title2=$\{P\}\ C\ \{Q\}$}

A <partial correctness> claim connecting a <precondition> $P$, a program $C$ and a <postcondition> $Q$: every terminating execution begun with $P$ ends with $Q$. State separately whether <total correctness> is intended.

 Back to article page