ウィキペディアがリストするループ不変条件を考えると、ループの最も弱い前提条件を生成する良い方法 ( http://en.wikipedia.org/wiki/Predicate_transformer_semanticsから):
wp(while E inv I do S, R) =
I \wedge
\forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] \wedge
\forall y. ((\neg E \wedge I) \implies R)[x <- y]
where y is a tuple of fresh variables.
M[x <- N] は、M 内のすべての x を N に置き換えます。
さて、私の問題は変数 y です。\forall y, は式で y をバインドするため、「y は新しい変数のタプルです」は解析されません。"[x <- y]" の y と同じように、y は \forall でバインドされていますか? 上記を解析することはできません。
編集：参照要求を避けるために言い換えました。
私の質問は、ループ不変条件と最も弱い前提条件の計算との間の直接的な関係は何かということです。実際に行われている多くのことは、ループの最も弱い前提条件を検証に適した前提条件に緩和しているようです。ウィキペディアの上記は、ループ不変条件が与えられた場合、鼻の最も弱い前提条件を実際に計算できることを示唆していますが、この条件を理解するのに苦労しています。