// precondition: idx is a valid index for array, A
AlgorithmXYZ ( A, idx )

1   key = A[idx]

2   i = idx - 1

3   while  i > 0  and  A[i] > key

4      A[i+1] = A[i]

5      i = i - 1

What is "loop invariant"?

 

 

What are i & idx at ...

 

     ... initialization?

 

     ... termination?

 

 

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