Loop invariant example

Document last modified:

A is an array of 3 integers

Sample Loop

Fill in:

values of A[] and i.

Label each row as loop invariant: Initialization, Maintenance, or Termination

Label each row as loop invariant: True or False.

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;
A[i]=2*A[i]; i = i + 1;
A[i]=2*A[i]; i = i + 1;
A[i]=2*A[i]; i = i + 1;