Loop invariant solution

Document last modified:

Sample Loop

int A[] = {5, 6, 7};

int i = 0;

//@ loop_invariant
          (\forall int j;
                 0 <= j && j < i;
                 A[j] == 2 * (\old(A[j]))

while( i < 3 ) {
A[i]=2*A[i];
i = i + 1;
}

Statement	(\forall int j; 0 ≤ j < i; A[j]==2*(\old(A[j]))	i	A[0]	A[1]	A[2]
int A[] = {5, 6, 7}; int i = 0;	Initialization empty so true	0	5	6	7
A[i]=2*A[i]; i = i + 1;	Maintenance true	1	10	6	7
A[i]=2*A[i]; i = i + 1;	Maintenance true	2	10	12	7
A[i]=2*A[i]; i = i + 1;	Maintenance true	3	10	12	14
	Termination true	3	10	12	14

Loop invariant: A[j]=2*A[j] for 0 ≤ j < i
In order for the loop invariant to be correct, it must hold for:
- Initialization: Before first test of the while condition
  
  i=0
  
  Therefore 0 ≤ j < 0 implies A[j] is empty and A[j]=2*A[j]
- Maintenance: State at end of executing the loop body
  
  Since A[i]=2*A[i] and i=i+1
  
  When i=0,1,2,3 then 0 ≤ j < i implies 0 ≤ j < 3 and A[j]=2*A[j]
  
  A[i]←2*old(A[i])        where old(A[i]) is the A[i] value before assignment
  
  Add 1 to i:
  
  i←i+1
  
  loop invariant A[j]=2*A[j] holds when 0 ≤ j < i.
- Termination: In order for the loop to terminate, the loop condition (i<3) does not hold, ensured by i=i+1 in loop.
After loop termination:

loop invariant holds

loop condition (i < 3) does not hold
When the loop terminates, know:

i=3

loop invariant A[j]=2*A[j] holds for 0 ≤ j < i

Therefore: A[j]=2*A[j] holds for 0 ≤ j < 3