3

给定一个循环不变量，维基百科列出了一个为循环生成最弱前提条件的好方法（来自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] 用 N 替换 M 中所有出现的 x。

现在，我的问题是变量 y。\forall y, 在表达式中绑定 y，因此“y 是新变量的元组”不会为我解析。\forall 中的 y 是否与 "[x <- y]" 中的 y 相同？我根本无法解析上述内容。

编辑：改写以避免参考请求。

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

4

1 回答 1

1

您引用的规则中的语法“x <- y”意味着我们可以假设分别命名为 x 1，x 2，... x n的几个变量同时替换为其他变量 y 1，y 2，... y n正如您所指出的，它在公式的上方由 \forall 绑定。

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

这就是维基百科文章所说的“while-loop 的最弱前提条件通常由称为循环不变量的谓词参数化I，以及表示<并称为循环变量的空间状态的有根据的关系”的意思。不仅是I必须事先选择好并且必须修饰程序，还有在循环体中修改S和出现在条件中的程序的若干变量的选择，以及E井的存在。这些变量的值的元组之间建立的顺序<保证了条件E最终为假。

这在实际验证系统中更容易理解，在这些系统中可以进行尝试。阅读本教程直到第2.3 节检查终止，看看相同解释的实用版本是否对您更有意义。

于 2014-10-12T00:30:13.230 回答