ループ変量

ループ $\mathtt{while}\ b\ \mathtt{do}\ c$ と表明 $I$ に対し、写像 $v : \Sigma \to \mathbb{Z}$ が次の 2 条件を満たすとき、$v$ を（不変条件 $I$ のもとでの）ループ変量という。

• （下に有界）$I(\sigma)$ かつ $\llbracket b \rrbracket\sigma = \mathrm{tt}$ ならば $v(\sigma) \ge 0$。
• （真に減る）すべての $k \in \mathbb{Z}$ について $\models [I \wedge b \wedge v = k]\ c\ [I \wedge v \lt k]$。ここで $v = k$ は表明 $\{\sigma \mid v(\sigma) = k\}$、$v \lt k$ は $\{\sigma \mid v(\sigma) \lt k\}$ を表す。