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

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 <- N] 将 M 中出现的所有 x 替换为 N。

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

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

我的问题是:循环不变量和计算最弱前提条件之间的直接联系是什么(如果有的话)。在实践中似乎做了很多事情将循环的最弱前提条件放宽到适合验证的前提条件。上面来自维基百科的内容表明，给定一个循环不变式，确实可以计算 Nose 上最弱的先决条件，但我很难理解这个条件。

Answer 1

您引用的规则中的语法“x <- y”表示同时替换我们可以假设命名为 x₁、x₂ 的几个变量, ... x_n 分别由其他变量 y₁, y₂, ... y_n 所指out, 在公式的正上方由\forall 绑定(bind)。

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

这就是维基百科文章所说的“while 循环的最弱前提条件通常由谓词参数化 I”的意思。称为循环不变量，空间状态上的一个有根据的关系表示为 <并称为循环变体。”它不仅仅是 I这肯定是事先选择好的，必须装饰程序，还有循环体中修改的一些程序变量的选择S并发生在 E 的情况下，以及有根据的订单的存在<这些变量值的元组之间保证条件 E最终是假的。

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