Question

For each pseudo-code function below (after the next ==== line), write a useful loop invariant capturing correctness for the
main loop in each of the following programs and briefly argue initialization, preservation, and termination.

EXAMPLE PROBLEM:

//Function to return the max of an array A
Maximum(array of integers A)
Local integer
integer m
m=0
for i = 1 to n
    if A[i] > m
        then m = A[i]
end function Maximum

EXAMPLE SOLUTION:  

The loop invariant is m = max(0, max_{1 \leq j \leq i-1} A[j]).

INITIALIZATION: at loop body entry, i=1 and m = 0, 
  so m=max(0, max_{1 \leq j \leq i-1}(A[j])=max(0, max_{1 \leq j \leq 0}A[j]).

PRESERVATION: if m=max(0, max_{1 \leq j \leq i-1} A[j]), then we have two cases: 

(1) If condition A[i] > m is true, then assignment m=A[i] makes m=max(0, max_{1 \leq j \leq i} A[j]),

(2) Otherwise if condition A[i] > m is false, then m is not assigned a new value and so remains unchanged, yet m=max(0, max_{1 \leq j \leq i} A[j]) since A[i] <= m.
In other words, at iteration i A[i] gets included in the calculation of maximum m.
Afterwards, incrementing i by 1 in the next iteration restores the invariant.

TERMINATION: when the loop terminates, i==n+1, so the invariant
implies m=max(0, max_{1 \leq j \leq n}A[j]) as desired.

======================================================================

E1.
//Function to return the value of x^2 for x>=1
Square(positive integer x)
Local integers
integers i,j
i=1
j=1
while i \noteq x do
    j=j + 2i + 1
    i=i + 1
end while
return j
end function Square

Answer 1

Loop invariant is an indermediate value that is true according to the given condition.

So lets see, what is invariant for above problem.

j=1,i=1

x=4

While (i! =x)

LOOP 1, while condituon is TRUE

j= 1+ 2*1+1=4,,//j is the invariant here

i=1+1=2

LOOP 2 while condition is TRUE

j=4+2*2+1=9

i=2+1=3

LOOP 3 while condition is TRUE

j= 9+ 2*3 +1 =16

i=4

LOOP 4, condition fails.

Now, you can se, the condition inside while fails, that is i==x, 4==4, so it comes out of the loop

Also, j=16, that is equal to x^2, that means invariant for this problem holds true as per the function specification.

Hope i helped you.