変量による停止性：全正当性の規則の健全性

$\mathcal{M}$ を解釈とする。

1. ループ $\mathtt{while}\ b\ \mathtt{do}\ c$ が、表明 $I$ のもとでループ変量 $v$ をもつならば、$\models_{\mathcal{M}} [I]\ \mathtt{while}\ b\ \mathtt{do}\ c\ [I \wedge \lnot b]$ である。
2. $\mathtt{call}$ を含まない命令について、定義 3.7 の (H-Skip)・(H-Assign)・(H-Seq)・(H-If)・(H-Conseq) は、三つ組を全正当性 $[P]\ c\ [Q]$ に読み替えても正しい。すなわち、各規則の前提の三つ組がすべて全正当ならば、結論の三つ組も全正当である。