Post-Assertions

A post-assertion is an assertion given at the end of a method (i.e. after the result or postcondition) that expresses one or more conditions that should be true when the method completes. Each condition should have something to say about the return value (for a function or operator) or the final values of modified objects (for a schema).

For example: in class Money we declared a division-by-integer operator that is supposed to round up the result. If our specification really does round up, we expect that as long we start with a nonzero amount, we end up with a nonzero result. We can express this expectation in a post-assertion like this:

    operator /(other: nat): Money
      pre other ~= 0
      ^= Money{(amount + other - 1) / other}
      assert amount ~= 0 ==> result.amount ~= 0;

By way of another example: multiplying a Money object by one should give a result equal to the original:

    operator *(other: nat): Money
      ^= Money{amount * other}
      assert other = 1 ==> result = self;

As a final example: calling the adjustPrice schema should not change what versions are available, neither should it affect the price of any version except the one specified. We can verify this by adding post-assertions:

schema !adjustPrice(ver: PublishedVersion, percent: int in (-99..99))
    post ( let gotVersion ^= ver in versions;
           [gotVersion]:
              version[ver]! = (version[ver] * (100 + percent))/100,
           []
         )
    assert versions'.dom = versions.dom,
           forall v::versions.dom :- v ~= ver ==> versions'[v] = versions[v];

Next: Expressing behaviours as properties