Hoare の三つ組：部分正当性と全正当性

$P, Q$ を表明、$c$ を言語 W の命令、$\mathcal{M}$ を解釈とする。

• 三つ組 $\{P\}\ c\ \{Q\}$ が $\mathcal{M}$ のもとで部分正当であるとは、すべての状態 $\sigma, \sigma'$ について「$P(\sigma)$ かつ $\langle c, \sigma \rangle \Downarrow \sigma'$ ならば $Q(\sigma')$」が成り立つことをいう。このとき $\models_{\mathcal{M}} \{P\}\ c\ \{Q\}$ と書く。
• 三つ組 $[P]\ c\ [Q]$ が $\mathcal{M}$ のもとで全正当であるとは、すべての状態 $\sigma$ について「$P(\sigma)$ ならば、$\langle c, \sigma \rangle \Downarrow \sigma'$ かつ $Q(\sigma')$ を満たす $\sigma'$ が存在する」が成り立つことをいう。このとき $\models_{\mathcal{M}} [P]\ c\ [Q]$ と書く。