Dafny - 从 Main 调用类方法后违反断言

Question

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

    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 块）不成立的错误，所以我选择了前两个确保（不确定它是否正确，但全班验证无误）。

无论如何，我遇到的问题来自于我从 main 调用 moreRuns() 时。我对返回的 bool 和 int 的断言似乎并不成立。有谁知道我哪里出错了？是我的后置条件还是我在调用 moreRuns() 之前忘记添加一些断言，或者我没有满足 val == 运行的选项？

任何提示将不胜感激！

Answer 1

您需要注意您在后置条件中比较的 runs 的值。当您修改 runs 时，您希望与 old(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 子句。