Dafny - 从 Main 调用类方法后的断言冲突

Question

我正在为一个将棒球运行初始化为0的类编写一些简单的代码。它唯一的方法应该是将运行次数作为其参数，并根据输入是否大于类变量和 int 以及 2 次运行中的较高者返回布尔值，如下所示：

class Baseball_Runs
{
var runs : int;
constructor()
ensures runs == 0;
{
runs := 0;
}
method moreRuns (val: int) returns (hasChanged: bool, newRuns: int)
requires val >= 0;
ensures (val > runs) ==> (hasChanged && newRuns == runs);
ensures (!hasChanged && newRuns == val) ==> (val <= runs);
//   ensures if (val > runs) then (hasChanged && newRuns == val) else (!hasChanged && newRuns == runs); 
modifies this;
{
if (val > runs)
{
hasChanged := true;
runs := val;
newRuns := val;
} else {
hasChanged := false;
newRuns := runs;
}
}
}
method Main()
{
var r := new Baseball_Runs();
var new_run: int := 0;
var hasChanged: bool := false;
var score: int;
score := 2;
hasChanged, new_run := r.moreRuns(score);
assert (hasChanged && new_run == 2);          // I get an assertion error here
}

我注释掉了第三个确保块，因为这是我第一次刺伤后条件，但它返回了一个错误，后置条件(else 块(不成立，所以我选择了前 2 个确保(不确定它是否正确，但整个类验证没有错误(。

无论如何，我遇到的问题源于我从main调用moreRuns((时。我对返回的布尔值和 int 的断言似乎站不住脚。有谁知道我哪里做错了？是我的后置条件还是我忘记在调用 moreRuns(( 之前添加一些断言，或者我没有迎合 val == 运行的选项？

任何提示将不胜感激！

Answer 1

您需要注意在后置条件中与哪个值进行比较runs值。当您修改要与old(runs)进行比较runs时。

以下版本的moreRuns工作：

method moreRuns (val: int) returns (hasChanged: bool, newRuns: int)
modifies this
requires val >= 0
ensures 
if val > old(runs)
then newRuns == val && hasChanged
else newRuns == old(runs) && !hasChanged
{
if (val > runs) {
hasChanged := true;
runs := val;
newRuns := val;
} else {
hasChanged := false;
newRuns := runs;
}
}

您不需要用分号结束modifies/requires/ensures子句。