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 ofA
become the lastN
elements ofB
- the
A'Length - N
last elements ofA
become the firstB'Length - N
elements ofB
.
This is of course equivalent to shifting all the elements of A
N
places to the left.
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
andB
should be of same lengthN
should be less than the length ofA
. Using a number greater thanA'Length
would yield the same result as usingN mod A'Length
.
The postconditions ensure that:
- the last
N
elements ofB
are equal to the firstN
elements ofA
- the
A'Length - N
last elements ofA
become the firstB'Length - N
elements ofB
.
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.