Guidelines for writing a Loop Invariant:

BEFORE YOU BEGIN ...

  1. Before you begin, if there is more than one loop, identify which you are considering.
  2. Before you begin, make SURE you understand exactly what the loop is doing. To do this, run the loop by hand on a smallish example. ("smallish" will depend on the pseudo code.)

THEN AND ONLY THEN...

  1. Identify all variables which have values before getting into the loop body.
  2. Make the strongest legitimate claim possible for the given code, using only those variables.
  3. Make a definitive statement of absolute fact.
    Do not include language which detracts from the INVARIANCE of your statement(s).
    if,   until,   while,   as long as...
  4. Use pseudo code conventions of your text. For example, when talking about some part of an array with specific index ranges....
                    

    A[ 1 .. j ]

    and not "A[1] thru A[j]"
    BTW, also applies when talking about growth classes... paren's below are REQUIRED.
                    

    Θ( n2 )

    and not "Θ n2"