Iota.org

The Iota algorithm

The Iota algorithm assign increasing values to an array, where the initial value is specified by the user. Its signature is the following:

procedure Iota (A : in out T_Arr ; Val : T);

For instance, let us suppose that A is an T array of size 5, then after a call Iota (A, 3), A will be (3, 4, 5, 6, 7). Notice that the incrementation step is not specified in the function signature.

The predicate Is_Iota

The predicate Is_Iota is be used to verify that an array has increasing values starting at a certain value. It is defined as follows:

function Is_Iota
  (A   : T_Arr;
   Val : T)
   return Boolean is
  (for all I in A'Range => A (I) = Val + T (I - A'First)) with
   Pre => Val + A'Length <= T'Last;

Notice that the precondition ensures that no overflow will happen.

Specification of Iota

The specification of iota is rather simple:

procedure Iota
  (A   : in out T_Arr;
   Val :        T) with
   Pre  => Val + A'Length <= T'Last,
   Post => Is_Iota (A, Val);

The precondition is necessary to prevent possible overflows, as we are dealing with numerical values.

Implementation of Iota

The implementation of iota is the following.

procedure Iota
  (A   : in out T_Arr;
   Val :        T)
is
   Count : T := Val;
begin
   for I in A'Range loop
      A (I) := Count;
      Count := Count + 1;
      pragma Loop_Invariant (Count = Val + T (I - A'First + 1));
      pragma Loop_Invariant (Is_Iota (A (A'First .. I), Val));
   end loop;
end Iota;

The loop invariants specify the fact that:

• Count is indeed a counter starting at Val and has the right value
• the predicate Is_Iota is verified for the sliced array A(A'First .. I).

Using GNATprove, everything is proved.