Dafny 验证 - 参考后状态中的原始变量

Question

我正在尝试在Dafny中验证我的代码，但遇到了一个问题：我有一个迭代序列并更改它的方法。该方法根据序列中的元素更改序列。我想添加一个这样的后置条件："如果序列中的元素是 X，那么应该会发生一些事情"。问题是该方法更改了集合（添加元素等），我想检查原始序列的条件。在达夫尼有没有一种优雅的方式？（我现在能想到的唯一方法是保持序列原始条件的全局变量，但我正在寻找正确的方法）。

代码示例：

method changeSeq(p: class1, s: seq<class1>)
ensures |s| == 10 ==> p in s
{
    if (|s| == 10){
        s := s + [p];
    }
}

在代码中，我希望 post 条件检查原始 s stat，而不是我们更改后的 stat。

Answer 1

您可以使用old来表示变量的旧值，例如s == old(s)。

下面是一个例子：http://rise4fun.com/Dafny/fhQgD

来自Dafny文档22.18。旧表达式

OldExpression_ = "old" "(" Expression(allowLemma: true, allowLambda: true) ")"

后置条件中使用旧表达式。 old(e)计算表达式e输入当前方法时具有的值。请注意，old 仅影响堆取消引用，如 o.f 和 a[i] 。特别是，old 对为局部变量或 out-parameter 返回的值没有影响。