dafny - Dafny 验证 - 参考 post 条件中的原始 var

Question

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

代码示例：

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对局部变量或输出参数的返回值没有影响。