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);
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.
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
.
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.