循环不变量和最弱前置条件有什么关系

Question

给定一个循环不变量，维基百科列表，一种为循环生成最弱前提条件的好方法 （来自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

现在，我的问题是变量 y。 \forall y, 在表达式中绑定 y，因此“y 是新变量的元组”不会为我解析。 \forall 中的 y 是否与 "[x

编辑：改写以避免引用请求。

我的问题是：循环不变量和计算最弱前提（如果有的话）之间的直接联系是什么。似乎在实践中所做的很多事情都将循环的最弱前提条件放松为适合验证的前提条件。来自维基百科的上述内容表明，给定一个循环不变量，确实可以计算出鼻子上最弱的先决条件，但我无法理解这个条件。

Answer 1

您引用的规则中的语法“x 1, x₂ , … x_n 分别由其他变量 y₁, y₂, … y_n 正如你所指出的那样出，在公式的正上方由 \forall 绑定。

在实践中应用规则的方法是选择出现在谓词R 中的一组变量。这些变量的数量和名称由应用规则的人选择，但必须可以在所选元组的元组之间定义有根据的关系<，这样\forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] 将是可证明的最终。

这就是维基百科文章的意思，当它说“while-loop 的最弱前提条件通常由称为循环不变量的谓词 I 参数化，并且在空间状态上的有充分根据的关系表示为 < 并称为循环变体。”不仅I必须预先选择并必须装饰程序，还有在循环体S中修改并在条件@987654329中发生的程序的多个变量的选择@，并且这些变量的值的元组之间存在有根据的顺序<保证条件E最终为假。

这在实际验证系统中更容易理解，可以在其中进行尝试。阅读this tutorial 直至2.3 检查终止部分，看看相同解释的实用版本是否对您更有意义。