The loop invariant is a statement that is true before and after each iteration of a loop. While the values of variables may change, it is the truth of the loop invariant that does not vary. Many statements can be made that are true both before and after each iteration of the loop, but the loop invariant must relate to the work that the loop does such that when the loop is finished the truth of the loop invariant implies the desired result.

The topic of loop invariance can help in loop construction.

Understanding a loop
Pre-condition - what must be true before the loop executes
Post-condition - what must be true when the loop has completed execution
Loop Variant - that which controls the execution of a loop, the exit condition
Loop Invariant - a statement that is true before and after each iteration of a loop

To check if a loop works

1. make sure the pre-condition is true before the loop starts
   
2. show that the pre-condition implies that the loop invariant is true
   
3. show that the execution of the loop variant (exit condition) does not as a side effect change the truth of the loop invariant
   
4. show that the loop invariant is true after execution of the statements in the body of the loop
   
5. show that upon termination of the loop the loop invariant implies the post-condition is true
   
6. show that each loop iteration decreases (or increases) the loop variant (exit condition)

	int sum = 0;
	int k = 0;
	while ( k < n )
	{
	     k ++;
	     sum = sum + k;
	}