Differences

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

--- invariant:ex5 [2007/02/27 16:07] – old revision restored 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 38: / Line 43: @@
 ----
-When done, remove the aspect from the build path and continue with the [[auth:intro|Authentication]] track.
+When done, remove the aspect from the build path and continue with the [[tracing:intro|Tracing]] track.