Dafny对带有break的循环了解多少？

Question

I am used to loops

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

没有任何中断，Dafny知道Inv && ! Grd是真的，但是: Dafny不检查break;命令后的循环不变量。因此

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";
}

显然，Dafny明白不变量不再成立。谁能告诉我达夫尼到底知道些什么。

Answer 1

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

这是一个更正式的答案：

在没有从循环中突然退出(如break)的情况下，证明Hoare三元组的常见方法

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

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

1. 检查循环不变量在进入循环时是否有效：

P ==> Inv

1. 检查循环不变量是否由循环体维护：

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

1. 检查不变守卫和否定守卫是否证明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的终点，你不需要证明任何东西，但是你必须在任何break上证明Q。

当Body包含其他break语句时，我刚才所说的也适用。这就是Dafny处理循环的方式(即，条件0加上重新表述的条件1和2，以及终止检查)。