Inner_Product.org

The Inner_Product algorithm

The Inner_Product algorithm computes the scalar product of two vectors A and B and adds it to an initial value Init. Its signature is:

function Inner_Product (A : T_Arr; B : T_Arr; Init : T) return T

The predicates used

The Multiply_No_Overflow predicate

This predicate will check if there will be an overflow due to the multiplication of two T values. Again, we should thank Claire Dross from AdaCore for the help and solution provided.

Looking at the Add_No_Overflow function previously defined, the specification of Multiply_No_Overflow could be:

function Multiply_No_Overflow
  (X, Y : T)
   return Boolean is
  (case X is when 0     => True,
     when -1            => Y /= T'First,
     when T'First .. -2 => Y in T'Last / X .. T'First / X,
     when 1 .. T'Last   => Y in T'First / X .. T'Last / X) with
   Contract_Cases => ((X * Y in T) => Multiply_No_Overflow'Result = True,
    others => Multiply_No_Overflow'Result = False);

Unfortunately, GNATprove cannot prove the contract of Multiply_No_Overflow. This is due to the fact that the properties we are trying to prove concern non-linear arithmetic and SMT solvers are not good at proving non-linear properties. We therefore need to write a complete implementation of Multiply_No_Overflow to help the provers to prove the contract cases.

The new specification of Multiply_No_Overflow is:

function Multiply_No_Overflow
  (X, Y : T)
   return Boolean with
   Contract_Cases => ((X * Y in T) => Multiply_No_Overflow'Result = True,
    others => Multiply_No_Overflow'Result = False);

And the corresponding implementation is:

function Multiply_No_Overflow
  (X, Y : T)
   return Boolean
is
   Res : Boolean;
begin
   case X is
      when 0 =>
	 Res := True;
      when -1 =>
	 Res := Y /= T'First;
      when T'First .. -2 =>
	 Res := Y in T'Last / X .. T'First / X;
	 pragma Assert (if Y < T'Last / X - 1 then X * Y > T'Last);
	 pragma Assert (if Y < T'Last / X then X * Y > T'Last);
      when 1 .. T'Last =>
	 Res := Y in T'First / X .. T'Last / X;
	 pragma Assert (if Y < T'First / X - 1 then X * Y < T'First);
	 pragma Assert (if Y < T'First / X then X * Y < T'First);
   end case;
   return Res;
end Multiply_No_Overflow;

The cases when X is equal to 0 or -1 are simple and do not need extra assertions. Let us consider the case when X is in the range T'First .. -2. Then we should check if Y is in the range T'Last / X .. T'First / X. The assertions guides the provers: if Y < T'Last / X then X * Y > T'Last which allows the prover to detect that we are in the second contract cases and must return False which is the case. The same reasoning applies for the case when X is in the range 1 .. T'Last.

Notice finally that we must use the -gnato13 switch for GNAT in order to be able to prove Multiply_No_Overflow (see numeric_algorithms.gpr file). -gnato13 signifies that overflows are strictly checked outside assertions and that they are eliminated inside assertions. This is due to the use of expressions like X * Y in assertions (cf. for instance the postcondition of Multiply_No_Overflows). Overflows could of course occur in such expressions as we also explore the case when there are, but we can reasonably remove overflow checks in assertions.

Using this implementation and specification, GNATprove proves the contract cases of Multiply_No_Overflow.

The Inner_Prod_Def_Rec and Inner_Prod_Def functions

Based on the Acc_Def_Rec function, we can write a similar function to calculate recursively the scalar product of two arrays.

function Inner_Prod_Def_Rec
  (A, B : T_Arr;
   F, L : Integer;
   Init : T)
   return T_Option is
  (if L < F then (True, Init)
   else
     (if
	Inner_Prod_Def_Rec (A, B, F, L - 1, Init).OK
	and then Multiply_No_Overflow (B (B'First + L), A (A'First + L))
	and then Add_No_Overflow
	  (Inner_Prod_Def_Rec (A, B, F, L - 1, Init).Value,
	   A (A'First + L) * B (B'First + L))
      then
	(True,
	 Inner_Prod_Def_Rec (A, B, F, L - 1, Init).Value +
	 B (B'First + L) * A (A'First + L))
      else (OK => False))) with
   Pre => A'Length = B'Length
   and then
   (if L >= F then L in 0 .. A'Length - 1 and F in 0 .. A'Length - 1);

The function is very similar, except for the fact that we have to first check if there is no overflow when multiplying the two values in the array before checking that there is no overflow when adding the product and the previous result.

As usual, the recursive call is encapsulated in a wrapper function:

function Inner_Prod_Def
  (A, B : T_Arr;
   F, L : Integer;
   Init : T)
   return T_Option is (Inner_Prod_Def_Rec (A, B, F, L, Init)) with
   Pre => A'Length = B'Length
   and then
   (if L >= F then L in 0 .. A'Length - 1 and F in 0 .. A'Length - 1);

Specification of Inner_Product

The specification of Inner_Product is the following:

function Inner_Product
  (A    : T_Arr;
   B    : T_Arr;
   Init : T)
   return T with
   Pre => A'Length = B'Length
   and then
   (for all J in 0 .. A'Length - 1 => Inner_Prod_Def (A, B, 0, J, Init).OK),
   Post => Inner_Product'Result =
   Inner_Prod_Def (A, B, 0, A'Length - 1, Init).Value;

The preconditions check that no overflow will occur during the algorithm. The postcondition checks that the result has to be the same than the one computed by the function Inner_Prod_Def.

Implementation of Inner_Product

The implementation of Inner_Product is quite simple:

function Inner_Product
  (A    : T_Arr;
   B    : T_Arr;
   Init : T)
   return T
is
   Result : T := Init;
begin
   for J in 0 .. A'Length - 1 loop

      pragma Assert (Inner_Prod_Def (A, B, 0, J, Init).OK);
      Result := Result + A (A'First + J) * B (B'First + J);

      pragma Loop_Invariant
	(Result = Inner_Prod_Def (A, B, 0, J, Init).Value);

   end loop;
   return Result;
end Inner_Product;

As in Accumulate, the assertion inside the loop is here to help the prover with the overflow checks.

Using this implementation and specification, GNATprove manages to prove everything (except the termination of Inner_Prod_Def_Rec as usual).