Reading material

Loop invariants

A loop invariant is also a predicate. It tells us something about the values of the variables while executing a loop. This predicate should be satisfied at the beginning of every iteration of the loop. Consider the loop
     while B do S
with loop invariant LI. If
     { LI B } S { LI },
that is, statement S preserves the loop invariant LI within the loop, then we can conclude that
     { LI } while B do S { LI B },
that is, if the loop invariant LI is satisfied at the start of the execution of the loop and the loop terminates then the loop invariant LI (and of course also B) is satisfied at termination.

Consider the following Java snippet.

int i = 1;
int x = 1;
while (i < N)
{
    x *= i + 1;
    i++;
}

Algorithm bubbleSort(sequence):
   Input: sequence of integers sequence
   Postcondition: sequence is sorted and contains the same integers as the original sequence
length length of sequence
i 0
while i < length do
     j 0
     while j < length - 1 do
         if jth element of sequence > (j+1)th element of sequence then
             swap jth and (j+1)th element of sequence

The outer loop has loop invariant
(A k : length - i <= k < length : (A l : k < l < length : kth element of sequence <= lth element of sequence))
and the inner loop has loop invariant
(A k : length - i <= k < length : (A l : k < l < length : kth element of sequence <= lth element of sequence))
(A k : 0 <= k < j : kth element of sequence <= jth element of sequence)

Question

public static void main(String[] args) 
{
    int lo = 1;
    int hi = 1;
    int n = Integer.parseInt(args[0]);
    int i = 1;
    while (i < n)
    { 
        int temp = hi;
	hi = lo + hi;
        lo = temp; 
	i++;    
    }
    System.out.println(hi);
}