Consider the following program fragment which has a while-loop. Assume there is an integer array a[ ] with length n.

int less = 0;

int k = 1;

while (k < n) {

if (a[k] <= a[0]) {

less++; /* Update less */

int temp = a[k]; /* Swap values in a[k] and a[less] */

a[k]= a[less];

a[less] = temp;

}

k++;

}

By using a loop invariant, prove that the program fragment has the following property:

Property: After the program fragment is completed,

• the values in {a[0], a[1], ..., a[less]} are at most a[0].
• the values in {a[less+1], a[less+2], ..., a[n-1]} are greater than a[0]

What is the loop invariant?

What is the initialization (base step)?

What is the maintenance step?

What is the termination?