Reverse_Copy.org

The Reverse_Copy algorithm

The Reverse_Copy algorithm inverts the order of the elements of a given array A in another array B without modifying A. Its signature is:

procedure Reverse_Copy (A : T_Arr; B : in out T_Arr);

The Is_Reversed predicate

In order to specify and implement the Reverse_Copy properly we will first define a predicate Is_Reversed in order to hide all quantifiers and make our code more readable. The predicate Is_Reversed is defined as follows:

function Is_Reversed
  (A : T_Arr;
   B : T_Arr)
   return Boolean is
  (for all I in A'Range => A (I) = B (B'Last - (I - A'First))) with
   Pre => A'Length = B'Length;

This predicate, on the condition that the two arrays given as parameters have the same length, will check whether the elements of A are in reverse order of those of B, i.e. A (A'Last) = B (B'First); A (A'Last -1) = B (B'First +1) ... and so on.

Specification of Reverse_Copy

Reverse_Copy can be specified as follows:

procedure Reverse_Copy
  (A :        T_Arr;
   B : in out T_Arr) with
   Pre  => A'Length = B'Length,
   Post => Is_Reversed (A, B);

The precondition verifies that A and B are of same length. The postcondition ensures that elements of A are indeed in the reverse order of those of B.

Implementation of Reverse_Copy

Reverse_Copy is implemented in the following way:

procedure Reverse_Copy
  (A :        T_Arr;
   B : in out T_Arr)
is
begin
   for J in B'Range loop
      B (J) := A (A'Last - (J - B'First));

      pragma Loop_Invariant
	(Is_Reversed
	   (B (B'First .. J), A (A'Last - (J - B'First) .. A'Last)));

   end loop;
end Reverse_Copy;

The implementation is straightforward, the loop invariant specifies that the sub-array composed of the first I-B'First elements of B is in reverse order of the sub-array of same length, composed of the last elements of A.

When using GNATprove on this implementation and specification, everything is proved.