Dafny不变量处理数据类型规则 循环不变量访问Node属性报错疑问

报错原因 #

Dafny对循环不变量的校验覆盖所有不变量需要生效的全场景，而非仅循环体执行阶段：

• 循环不变量需要满足三个阶段的合法性和成立要求：首次进入循环前、每次循环体执行结束后、循环终止时
• 你的循环终止条件为working.Node?为假，即终止时working为Empty类型。原不变量r==true ==> (working.value == s)未限制r为真时working的类型，若r为真就会触发Empty类型访问value属性的非法操作，因此Dafny提前抛出类型错误
• 注释不变量后Dafny不再校验该表达式合法性因此无报错；循环体内的断言可通过，是因为循环体执行时循环条件working.Node?必然为真，Dafny可确认此时working为Node类型

修复方案 #

只需在不变量的蕴含逻辑中先补充working.Node?的判断，保证访问working.value前类型合法即可，修复后的完整代码如下：

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.Node? && (working.value == s)
      {
         r:=false; 
         working:= working.right;
         assert r==true ==>  (working.value == s);
      }
    }
    r:=false;
    assert r==true ==>  (working.value == s);
}

内容的提问来源于stack exchange，提问作者david streader