1   j = 9

2   for i = 0 to 9

3     j = j - 1                // j--

What is "loop invariant"?

 

 

What are i & j at ...

 

     ... initialization?

 

     ... termination?

 

 

Prove loop invariant holds at initialization, mantenance, and termination.