A Loop Invariant says what is true at the top of every loop?

\[ \begin{array}{l} \textbf{begin routine } \langle \text{pre-cond} \rangle \\ \quad \text{code pre-loop} \quad \text{% Establish loop invariant} \\ \quad \textbf{loop } \langle \text{loop-invariant} \rangle \\ \quad \quad \textbf{exit when } \langle \text{exit-cond} \rangle \\ \quad \quad \text{code loop} \quad \text{% Make progress while maintaining invariant} \\ \quad \textbf{end loop} \\ \quad \text{code post-loop} \quad \text{% Clean up loose ends} \\ \quad \langle \text{post-cond} \rangle \\ \textbf{end routine} \end{array} \]

Loop Invariant Template

  1. Specifications (Pre/Post)
  2. Define Loop Invariant
  3. Take a step
  4. Maintain the Loop Invariant
  5. Exit
  6. Establish the Loop Invariant
  7. Obtain the Post Condition
  8. Running Time

Types of loop invariants

Sources

These are just outlining the steps found at the link below. Make sure you understand what you should be doing in each step.