Differences

This shows you the differences between two versions of the page.

--- invariant:ex5 [2007/02/26 10:41] – created bdefrain
+++ invariant:ex5 [2021/02/05 13:53] (current) – external edit 127.0.0.1
@@ Line 1: / Line 1: @@
-====== Invariants: Postconditions ======
+[[invariant:intro|Intro]]
+[[invariant:ex1|Ex1]]
+[[invariant:ex2|Ex2]]
+[[invariant:ex3|Ex3]]
+[[invariant:ex4|Ex4]]
+[[invariant:ex5|Ex5]]====== Invariants: Postconditions ======
 ===== Point Move Postcondition =====
@@ Line 11: / Line 16: @@
 </note>
-When the access to the old coordinates and move arguments has been established, the check comes down to essentially the following code:
+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>
@@ Line 22: / Line 27: @@
 ===== 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.