Rotate_Copy.org

The Rotate_Copy algorithm

The Rotate_Copy algorithm executes a rotation on the elements of an array, and stores the result in another array:

procedure Rotate_Copy (A : T_Arr; N : Positive; B : in out T_Arr)

The resulting array B is defined as follows:

• the first N elements of A become the last N elements of B
• the A'Length - N last elements of A become the first B'Length - N elements of B.

This is of course equivalent to shifting all the elements of A N places to the left.

Specification of Rotate_Copy

The specification of Rotate_Copy is:

procedure Rotate_Copy
  (A :        T_Arr;
   N :        Positive;
   B : in out T_Arr) with
   Pre  => A'Length = B'Length and then N < A'Length,
   Post => A (A'First .. A'First + (N - 1)) = B (B'Last - (N - 1) .. B'Last)
   and then A (A'First + N .. A'Last) = B (B'First .. B'Last - N);

The precondition express that:

• A and B should be of same length
• N should be less than the length of A. Using a number greater than A'Length would yield the same result as using N mod A'Length.

The postconditions ensure that:

• the last N elements of B are equal to the first N elements of A
• the A'Length - N last elements of A become the first B'Length - N elements of B.

Implementation of Rotate_Copy

Rotate copy is implemented using the Copy function defined previously:

procedure Rotate_Copy
  (A :        T_Arr;
   N :        Positive;
   B : in out T_Arr)
is
begin
   Copy (A (A'First + N .. A'Last), B (B'First .. B'Last - N));
   Copy (A (A'First .. A'First + (N - 1)), B (B'Last - (N - 1) .. B'Last));
end Rotate_Copy;

GNATprove does not require additional annotations in order to prove this program.