Reverse an Array

If you wish to do this assignment, consult with the instructor for help getting started.

• Write a sequential program to reverse an array in-place.

• Formulate a model of your program in PVS:

  Reverse(A: ARRAY[nat->T], L:nat, U:{i:nat | l <= i}): RECURSIVE ARRAY[nat->T] = ...

  Reverse(A, L, U) takes an array A with lower and upper bounds L and U, with L ≤ U.

• Reverse(A, L, U) models the effect of the program on A by returning an array whose elements in the range [L..U] in reverse order of the elements in A[L..U].

  Reversed?(A, B: ARRAY[nat->T], L:nat, U:{i:nat | l <= i}): bool = FORALL (k: {i: nat | i <= U-L): A(L+k) = A(U-k)

Notes and Comments

• Read Section 1.2.2 of the Sorting Tutorial [PDF] to learn about better ways to handle index ranges. The tutorial also gives a detailed example of representing a sequential program in PVS.

• A loop of the form

  while test do {body}

  is represented as an iterative function

  Loop(x, y, z): RECURSIVE state = IF NOT test THEN value ELSE Loop( {effect of body on x, y, z}) ENDIF MEASURE { some measure}

• A nested loop

  while test1 do {    while test2 do { body }    }

  is similarly represented by nested function calls

  InnerLoop(x, y, z): RECURSIVE state = IF NOT test2 THEN value2 ELSE InnerLoop( {effect of body on x, y, z}) ENDIF MEASURE { some measure} OuterLoop(x, y, z): RECURSIVE state = IF NOT test1 THEN value1 ELSE OuterLoop( InnerLoop(x, y, z)) ENDIF MEASURE { some measure}