User Tools

Site Tools


invariant:ex5

This is an old revision of the document!


Invariants: Postconditions

Point Move Postcondition

Task: Pass tests.PointMovePostcondition.

A postcondition of the move operation of a Point is that the coordinates should change accordingly. If a call to move didn't actually move a point by the desired offset, then the point is in an illegal state and so an IllegalStateException should be thrown.

Tools: around advice. Note that because we're dealing with how the coordinates change during move, we need access to the coordinates both before and after the move, in one piece of advice.

When the access to the old coordinates and move arguments has been established, the check comes down to essentially the following code:

if(p.getX() - oldx != dx || p.getY() - oldy != dy)
  throw new IllegalStateException();

With a correct implementation, you should pass the tests of suite tests.PointMovePostcondition.

Bounds Move Postcondition

invariant/ex5.1172482886.txt.gz · Last modified: 2007/02/26 10:41 by bdefrain