为什么这个前提会失败，我不太明白

Question

datatype message = Nil | Aenc(aencMsg:message,aencKey:message) | Senc(m1:message,m2:message) | K(r1:role,r2:role) | Pk(r:role) | Sk(r:role) | Str(r:role) | Var(n:role) | Concat(array<message>)
type channel = array<message>
method ReceiveMsgFromChannel(c:channel) returns (m:message)
requires c.Length > 0 
requires c[0] != Nil
ensures  c[0] == Nil
// requires verify(c)
modifies c
{
m:=c[0];
c[0]:=Nil;
}
method AliceSendMsg_1(c:channel)
requires c.Length > 0
modifies c
{
var aencMsg:=new message[2];
aencMsg[0]:=Var("Na");
aencMsg[1]:=Str("A");
var m :=Aenc(Concat(aencMsg),Pk("B"));
c[0] :=m;
assert m.aencKey == Pk("B");
}
method Test(ch1:channel)
requires ch1.Length>0
requires forall i:int :: 0<=i<ch1.Length ==> ch1[i]==Nil
modifies ch1
{
AliceSendMsg_1(ch1);
var m1:=ReceiveMsgFromChannel(ch1);
}

这是我代码的一部分。我试图在协议中定义两个实体，一个发送消息，另一个接收消息。其中AliceSendMsg_1代表Alice发送aenc的消息而不是Nil。然后Bob从Channel接收消息。但信息不可能是否定的。预配置失败的原因。如有任何帮助，我们将不胜感激。非常感谢。

Answer 1

Test的主体首先执行

AliceSendMsg_1(ch1);

此外，AliceSendMsg_1用modifies ch1标记，但不给出任何后置条件。因此，当Dafny对方法Test进行推理时，它对调用AliceSendMsg_1之后ch1的内容一无所知。请记住，当Dafny验证Test时，它不会查看AliceSendMsg_1的主体。关于AliceSendMsg_1，它所知道的只是该方法的签名中的内容。

您可以通过简单地将所需的属性添加到AliceSendMsg_1的签名中来解决此问题。

method AliceSendMsg_1(c:channel)
requires c.Length > 0 
ensures c[0] != Nil  // add this line
modifies c