调用可能违反上下文的修改子句

Question

我正在写一个愚蠢的代码来验证一个函数，它改变了队列的头和尾，函数本身被验证但是当我添加主函数时，我得到错误：调用可能违反上下文的修改子句，我的方法中没有任何新内容，因此无需编写 ensures fresh。不知道是什么问题，谁能帮帮我。

    class Quack<Data>
    {
        var buf: array<Data>;
        var m: int, n: int;

        ghost var shadow: seq<Data>;

        predicate Valid() reads this, this.buf
        { buf!=null && buf.Length!=0 && 0<=m<=n<=buf.Length && shadow==buf[m..n] }
    ...
        method HeadTail() modifies this, this.buf
    requires Valid()
    ensures Valid()
    ensures buf.Length == old(buf.Length)
    ensures |shadow| == |old(shadow)|
    ensures n == old(n) && m == old(m)
    ensures if n-m > 1 then (shadow[0] == buf[m] == old(buf[n-1])) && (shadow[|shadow| - 1] == buf[n-1] == old(buf[m]))
                            && shadow[1..|shadow| - 1] == old(shadow[1..|shadow| - 1])
                            && forall i:: (0 <= i < buf.Length && i != m && i != n-1) ==> (buf[i] == old(buf[i]))
            else buf == old(buf) && shadow == old(shadow)
    { 
        if(n-m > 1){
            buf[n-1], buf[m] := buf[m], buf[n-1];
            shadow := [buf[m]] + shadow[1..|shadow| - 1] + [buf[n - 1]];
        }
    }
}

        method Main()
        {   var q:= new Quack<char>(10);
            var l: char;
            q.Push('r'); q.Push('s'); q.Push('k'); q.Push('o'); q.Push('w');
            l:= q.Pop(); assert l=='w'; print l;  
            q.HeadTail();
            l:= q.Qop(); assert l=='o'; print l;
            l:= q.Pop(); assert l=='r'; print l;
            q.HeadTail();
            l:= q.Qop(); assert l=='k'; print l;    
            q.HeadTail();
            l:= q.Qop(); assert l=='s'; print l;        
            var e: bool:= q.Empty();
            if e {print "\nqueue empty\n";} else {print "\nqueue not empty\n";}
        }

错误发生在我在main中调用q.HeadTail()的第二次和第三次；

Answer 1

方法HeadTail()说它修改了this和this.buf。方法 Main 在 q 上调用 HeadTail，这意味着该调用修改了 q 和 q.buf。方法Main做一个new得到q，所以允许Main修改q。但是没有关于 q.buf 是什么的信息。要修改q.buf，Main必须证明q.buf是新分配的（即从Main开始分配的；换言之，q.buf必须是新鲜到 Main)。

我看不到你对构造函数的说明和 Push，但我怀疑你需要在构造函数的后置条件中说 fresh(buf)。然后，作为 Push 的后置条件，您可以编写

ensures buf == old(buf) || fresh(buf)

然而，如果你的 Quack class 永远不会改变 buf （我不知道它是否改变），那么声明 buf 不可变：

const buf: array<Data>

鲁斯坦

Answer 2

Dafny 只会修改确保新鲜的数组，这意味着它自己分配了数组 - 请记住 buf 只是一个指针！你必须在 HeadTail 中包含 ensures buf == old(buf) 以告诉 Dafny buf 仍然是新鲜的（这样，断言从以前的一些方法中使用 ensures fresh(buf) 继承而来）。

如您所见，HeadTail 第一次调用时不会失败，因为 fresh(buf) 之前已被断言，但是在丢失此知识后立即 - 导致第二次调用 HeadTail 违反修改条款。

调用可能违反上下文的修改子句

call may violate context's modifies clause

dafny