iteration - Dafny 对带中断的循环了解多少？

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

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

Answer 1

如果有break语句，则循环后的条件为Inv && !Grd 的析取和满足条件各自的 break 语句。

这是一个更正式的答案:

在循环中没有任何突然退出(例如 break)的情况下，熟悉的证明霍尔三元组的方法

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

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

检查循环不变量在循环入口处是否成立:

P ==> Inv

1. 检查循环体是否维护了循环不变式:

{{ 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 }}

你不必沿着任何到达的路径进一步证明任何事情一个中断。证明义务 2 可以用一种双重方式重新表述:

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

我的意思是，如果你到达...Body的末尾，你就不必证明任何事情，但你必须在任何中断处证明Q。

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