Loop invariant - Too Weak

Sample Loop

Loop invariant: i ≤ A.length

• The loop invariant is correct, but it is too weak.
   
• It only makes a statement about the value of i.
   
• It does not state what the values of A will be.

int A[] = {5, 6, 7}; int i = 0; //@ loop_invariant (i ≤ A.length); while( i < A.length ) {           A[i]=2*A[i];           i = i + 1; }

Statement Object Values   i=0 A.length = 3 //@ loop_invariant (i ≤ A.length); while( i < A.length ) { }   State at time of loop exit i = 3 A.length = 3

• In this example, when the loop terminates, we know:
  • i=3
  • A.length = 3
  • Therefore: i ≤ A.length
  • But we don't know if A[j]=2*A[j] for 0 ≤ j < i

   

• It is the responsibility of the software developer to write a loop invariant that is both correct and strong enough.