dafny 不变量如何处理数据类型

Question

示例代码似乎是人为的，因为它是我能找到的用于说明我的问题的最小代码。

datatype Twee = Node(value : int, left : Twee, right : Twee) | Empty
method containsI(t : Twee, s : int) returns (r : bool) 
{
    var working :Twee := t;
    if (working.Node?) {
       r:= (working.value == s);
       assert r==true ==>  (working.value == s);
      while working.Node?
         decreases working
         invariant r==true ==>  (working.value == s)
      {  //assert r==true ==>  (working.value == s);
         r:=false; 
         working:= working.right;
         assert r==true ==>  (working.value == s);
      }
    }
    r:=false;
    assert r==true ==>  (working.value == s);
   }

Dafny 在不变量中抱怨 working.value。声明它只能在工作是Node 事件时应用，尽管当不变量被注释掉时，Dafny 报告没有问题。因此，Dafny 似乎知道工作是Node。

非常感谢任何对我的理解的更正。

Answer 1

循环不变量需要在循环的每次迭代之前和之后保持；特别是，当循环条件返回 false 时，它​​应该保持循环终止。

例如，循环体中的任何内容都由working.Node? 保护（如working:= working.right; 行），这就是Dafny 报告没有问题的原因。但是，Dafny 报告线路有问题 invariant r==true ==> (working.value == s) 因为这个表达式可能需要在 working.Node? 确实不成立的上下文中进行评估。

也许你的意思是写类似的东西

invariant r==true ==> working.Node? ==> (working.value == s)

很难说出你的意图是什么。

顺便说一句，你可能想知道为什么最后的两行没有失败...

    r:=false;
    assert r==true ==>  (working.value == s);

这是因为断言在这里是一个空洞的谓词（r==true 总是计算为false）