为什么 Dafny 认为在使用 ghost 变量时这个前提条件可能会有问题？

Question

假设我有以下 class:

class Testing {
    ghost var myGhostVar: int;

    method Init() 
    modifies this
    ensures this.myGhostVar == -1    
    {
        this.myGhostVar := -1;
        assert this.myGhostVar == -1;
    }


    method MyTestingMethod(list: array<int>, t: int)
    modifies this
    requires list.Length > 1
    requires this.myGhostVar == -1
    requires t == -1
    ensures MyPredicate(list, myGhostVar)
    ensures this.myGhostVar < list.Length
    {
        this.Init();
        assert this.myGhostVar < 0;
        assert list.Length > 0;
        assert this.myGhostVar < list.Length;
    }

    predicate MyPredicate(list: array<int>, startIndex: int)
    requires startIndex < list.Length
    {
        true
    }
}

出于某种原因，Dafny 说对 MyPredicate(...) 的调用可能无法保持。但是，如果我改为使用 t 而不是 myGhostVar 作为参数；达夫尼没有怨言。

两者都有相同的 requires 谓词，这让人有点困惑。使用幻影变量时我是否遗漏了什么？

Answer 1

这不是幽灵变量的问题 - 您可以检查一下，如果删除 ghost 关键字，您会遇到同样的问题。

问题是要调用MyPredicate(list, myGhostVar)，你需要满足前置条件，这里是myGhostVar < list.Length。

你的 ensures 子句中居然有这个条件，太棒了！

    ensures MyPredicate(list, myGhostVar)
    ensures this.myGhostVar < list.Length

但是您对 MyPredicate 的调用在您需要的条件之前。尝试翻转顺序：

    ensures this.myGhostVar < list.Length
    ensures MyPredicate(list, myGhostVar)

你应该会看到 Dafny 不再抱怨了。

一般来说，Dafny 会尝试使用 previous 确保子句来证明 ensures 子句中的先决条件成立。

Both have the same requires predicate which makes it all a bit confusing. Is it something that I am missing when using ghost variables?

在这里，我想你问的是条款

    requires this.myGhostVar == -1
    requires t == -1

并想知道为什么它不能使用 this.myGhostVar == -1 前置条件来证明 this.myGhostVar < list.Length。

答案是 this.myGhostVar == -1 是一个前提条件，这意味着 Dafny 知道它在进入时保持不变，但 this.myGhostVar 的值可能会在方法执行期间发生变化。所以这对 Dafny 检查 post 条件没有帮助。

请注意，Dafny 在检查其 post 条件的格式是否正确时不会查看其方法的主体。为此，Dafny 只知道您在方法签名中告诉它的内容。

为什么 Dafny 认为在使用 ghost 变量时这个前提条件可能会有问题？

Why does Dafny think there might be a problem with this precondition when using a ghost variable?

dafny