User Tools

Site Tools


invariant:ex5

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
invariant:ex5 [2007/02/27 16:07] bdefraininvariant: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 ===== ===== Point Move Postcondition =====
Line 11: Line 16:
 </note> </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)+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> <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.
invariant/ex5.1172588824.txt.gz · Last modified: 2007/02/27 16:07 by bdefrain