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
    }
我注释了第三个确保块，因为这是我在后置条件下的第一个刺，但它返回一个错误，其中后置条件（其他块）不成立，因此我使用前两个确保（不知道它是否正确）但整个课程都经过验证，没有错误）。

无论如何，当我从main调用moreRuns（）时出现了我遇到的问题。我对bool和int返回的主张似乎不成立。有人知道我哪里出问题了吗？是我的后置条件，还是在调用moreRuns（）之前忘记添加一些断言，还是我不满足val ==运行的选项？

任何提示将不胜感激！

我正在为将棒球奔跑次数设为0的类编写一些简单的代码。它的唯一方法应该将奔跑次数作为其参数，并根据是否... ...返回布尔值。]] >

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

[C0的以下版本有效：

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子句。

Answer 1

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