[[invariant:intro|Intro]]
[[invariant:ex1|Ex1]]
[[invariant:ex2|Ex2]]
[[invariant:ex3|Ex3]]
[[invariant:ex4|Ex4]]
[[invariant:ex5|Ex5]]====== 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.

<note tip>
**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.
</note>

When the access to the old coordinates and move arguments has been established, the check comes down to essentially the following code: (where ''dx'' and ''dy'' are the arguments given to the ''move'' operation)

<code aspectj>
if(p.getX() - oldx != dx || p.getY() - oldy != dy)
  throw new IllegalStateException();
</code>

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

===== Bounds Move Postcondition =====

**Task:** Pass ''tests.BoundsMovePostcondition''.

''FigureElement'' objects have a ''getBounds()'' method that returns a ''[[http://java.sun.com/j2se/1.5.0/docs/api/java/awt/Rectangle.html|java.awt.Rectangle]]'' representing the bounds of the object. An important postcondition of the general ''move'' operation on a figure element is that the figure element's bounds rectangle should move by the same amount as the figure itself. Write an aspect to check for this postcondition -- throw an ''IllegalStateException'' if it is violated.

<note tip>
The check can be less technical than in the previous case if you employ the ''Rectangle'' API:

  - Employ the [[http://java.sun.com/j2se/1.5.0/docs/api/java/awt/Rectangle.html#Rectangle(java.awt.Rectangle)|copy constructor]] to create a clone of the original bounds.
  - Replay the move on the clone with the ''[[http://java.sun.com/j2se/1.5.0/docs/api/java/awt/Rectangle.html#translate(int,%20int)|translate]]'' method.
  - Compare the result to the actual new bounds using the ''[[http://java.sun.com/j2se/1.5.0/docs/api/java/awt/Rectangle.html#equals(java.lang.Object)|equals]]'' method. 
</note>

A correct implementation should pass the tests of suite ''tests.BoundsMovePostcondition''.

----

When done, remove the aspect from the build path and continue with the [[tracing:intro|Tracing]] track.