The Fill
algorithm initializes an array with a particular
value. Here is its signature:
procedure Fill (A : in out T_Arr; Val : T);
A
needs of course to be passed as a out
parameter as it will be
modified, but also as an in
parameter because it will be used
with the Constant_Range_From_Location
predicate defined with the
Search_N algorithm and Constant_Range_From_Location
requires a
in
parameter.
The specification of Fill
is very simple:
procedure Fill
(A : in out T_Arr;
Val : T) with
Pre => A'Length > 0,
Post => Constant_Range_From_Location (A, Val, A'First, A'Length);
The implementation of Fill
is the following:
procedure Fill
(A : in out T_Arr;
Val : T)
is
begin
for I in A'Range loop
A (I) := Val;
pragma Loop_Invariant
(Constant_Range_From_Location (A, Val, A'First, I - A'First + 1));
end loop;
end Fill;
The loop invariant specify that there is a constant range of Val
values starting at index A'First
with length I - A'First + 1
in A
.
Everything is easily proved with GNATprove
.