Dafny - Assertion violation after calling class method from Main

Question

I'm writing up some simple code for a class which intializes baseball runs to 0. Its only method is supposed to take in the number of runs as its parameter, and return a bool based on whether the input was larger than the class variable and an int, and the higher of the 2 runs as follows:

    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
    }

I commented out the 3rd ensures block as that was my first stab at the post-condition but it returns an error where the postcondition (else block) does not hold, so I went with the first 2 ensures (not sure if it's correct but the whole class verified without error).

Anyhow, the problem I'm getting arises from when I'm calling the moreRuns() from main. My assertion for the bool and int returned doesn't seem to hold. Does anyone know where I went wrong? Was it my post-condition or did I forget to add some assert before calling moreRuns() or did I not cater for the option where val == runs?

Any tips would be greatly appreciated!

Answer 1

You need to be careful which value of runs you're comparing to in your post-condition. As you are modifying runs you want to compare to old(runs).

The following version of moreRuns works:

        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;
            }
        }

You don't need to end modifies/requires/ensures clauses with a semicolon.