为什么 Dafny 认为在使用 ghost 变量时这个前置条件可能存在问题？答案

【问题标题】：Why does Dafny think there might be a problem with this precondition when using a ghost variable?为什么 Dafny 认为在使用 ghost 变量时这个前置条件可能存在问题？
【发布时间】：2019-12-18 18:28:54
【问题描述】：

假设我有以下课程：

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 谓词，这使得这一切都有些混乱。是不是我在使用 ghost 变量时遗漏了什么？

【问题讨论】：

标签： dafny

【解决方案1】：

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

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

您的 ensure 子句中实际上有这个条件，这很棒！

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

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

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

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

通常，Dafny 会尝试使用 previous Ensure 子句来证明 ensures 子句中的前置条件成立。

两者都有相同的 requires 谓词，这使得它有点混乱。是不是我在使用 ghost 变量时遗漏了什么？

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

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

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

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

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

【讨论】：