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";
}
显然达夫尼明白不变量不再成立。谁能告诉我达夫尼到底知道什么。
最佳答案
如果有break
语句,则循环后的条件为
Inv && !Grd
的析取和满足条件
各自的 break
语句。
这是一个更正式的答案:
在循环中没有任何突然退出(例如 break
)的情况下,熟悉的
证明霍尔三元组的方法
{{ 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 }}
你不必沿着任何到达的路径进一步证明任何事情
一个中断
。
证明义务 2 可以用一种双重方式重新表述:
{{ Inv }}
if !Grd {
break;
}
Body
{{ break: Q }}
我的意思是,如果你到达...Body
的末尾,你就不必证明任何事情,
但你必须在任何中断
处证明Q
。
当 Body
包含其他 break
语句时,我刚才所说的也适用。这就是 Dafny 处理循环的方式(即条件 0 加上改写的条件 1 和 2,加上终止检查)。
关于iteration - Dafny 对带中断的循环了解多少?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/63800693/