Dafny对中断循环了解什么？

问题描述

I am used to loops

while Grd
invariant Inv
{ ..}
assert Inv && !Grd;

在没有任何中断的情况下，达夫尼知道Inv && ! Grd是正确的，但：在break;命令之后，Dafny不检查循环不变式。因此

method tester(s:seq<int>) returns (r:int) 
ensures r <= 0
{   var i:nat := |s|;
    r := 0;
    while (i > 0)
       decreases i
       invariant r == 0;
    {   i := i -1;
        if s[i]< 0  { r:= s[i]; break;}        
    }    
   // assert r == 0; // invariant dose not hold
}

method Main() {
    var x:int := tester([1,-9,0]);
    print x,"\n";
}

很显然，达夫尼知道不变式不再成立。谁能告诉我达芙妮到底知道些什么。

解决方法

如果有break条语句，则循环后的条件是 Inv && !Grd的析取和在相应的break语句。

这是一个更正式的答案：

在没有任何突然退出（例如break）的情况下，熟悉的证明Hoare三元组的方法

{{ P }}
while Grd
  invariant Inv
{
  Body
}
{{ Q }}

是为了证明以下三个条件（我忽略终止）：

检查循环不变式是否在进入循环时成立：

P ==> Inv

检查循环不变性是否由循环主体维护：

{{ Inv && Grd }}
Body
{{ Inv }}

检查不变且否定的后卫是否证明Q：

Inv && !Grd ==> Q

让我重新描述条件1和2。为此，我将从将while循环重写为带有中断的永远重复循环：

loop
  invariant Inv
{
  if !Grd {
    break;
  }
  Body
}

（换句话说，我使用loop作为while true。）以上证明义务1 现在可以改写为证明

{{ Inv }}
if !Grd {
  break;
}
Body
{{ Inv }}

您不需要的地方必须沿到达的任何路径进一步证明一切 break。证明义务2可以用双重方式重新表达：

{{ Inv }}
if !Grd {
  break;
}
Body
{{ break: Q }}

我的意思是，如果您到达...Body的末尾，则无需证明任何内容，但是您必须在任何Q上证明break。

当Body包含其他break语句时，我刚才所说的内容同样适用。 Dafny就是这样处理循环的（即条件0加上改写的条件1和2，再加上终止检查）。

break dafny iteration iteration