-1

我正在为一个将棒球运行初始化为 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 块）不成立的错误，所以我选择了前两个确保（不确定它是否正确但全班验证无误）。

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

任何提示将非常感谢！

4

1 回答 1

0

您需要注意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

于 2019-11-26T15:19:53.197 回答