Writing Specifications and Proving Correctness

Consider the following program fragment:

     int i = 1;
     int j = num;
     while (i < j) {
         int t = A[i];
         A[i] = A[j];
         A[j] = t;
         i++;
         j--;
     }

Question 21

What does this program fragment do?

Question 22

Let newA represent the value of array A after the code has executed. Which of the following statements is the best postcondition for this code?

Question 23

Is the statement

     num < A.length 

Exercise 24

Give a loop invariant for this while loop that relates i and j. Make it as strong a statement as possible.

Question 25

Which one of the following statements is NOT a loop invariant for this while loop?