Skip to content

Latest commit

 

History

History
255 lines (205 loc) · 7.77 KB

Accumulate.org

File metadata and controls

255 lines (205 loc) · 7.77 KB

The Accumulate algorithm

The Accumulate algorithm will compute the sum of the elements of an array. Its signature reads:

function Accumulate (A : T_Arr; Init : T) return T;

The algorithm will return Init + A (A'First) + A (A'First+1) + ... + A (A'Last).

This algorithm is the first in this chapter to present difficulties when proving that no overflow may happen. We will present two versions of this algorithm, one which tries to “naively” handle the overflow checks, and another version which correctly deals with overflows.

A naive Accumulate

Predicates used

To be able to write the preconditions and postconditions of Accumulate we first need to write a predicate defining what the result of our function should be:

function Acc_Def_Rec
  (A    : T_Arr;
   Init : T)
   return T is
  (case A'Length is when 0 => Init,
     when others           =>
       Acc_Def_Rec (A (A'First .. A'Last - 1), Init) + A (A'Last));
function Acc_Def
  (A    : T_Arr;
   Init : T)
   return T is (Acc_Def_Rec (A, Init));

As usual with a recursive function, we encapsulate the call to the recursive function into a simple function in order to be able to use it as a postcondition. A pragma Annotate for Acc_Def_Rec is also defined to assert that the recursive function terminates.

Specification of Accumulate

With the given predicates we can write a specification for Accumulate:

function Accumulate_Naive
  (A    : T_Arr;
   Init : T)
   return T with
   Pre  => (for all I in A'Range => Acc_Def (A (A'First .. I), Init) in T),
   Post => Accumulate_Naive'Result = Acc_Def (A, Init);

The precondition expresses that all the intermediary sums we are going to evaluate should not overflow. The postcondition expresses that our algorithm returns the correct value.

Implementation of Accumulate

An implementation satifying our specification is the following

function Accumulate_Naive
  (A    : T_Arr;
   Init : T)
   return T
is
   Result : T := Init;
begin
   for I in A'Range loop

      pragma Assert (Acc_Def (A (A'First .. I), Init) in T);
      Result := Result + A (I);
      pragma Loop_Invariant (Result = Acc_Def (A (A'First .. I), Init));

   end loop;
   return Result;

end Accumulate_Naive;

The assertion in the loop verifies that there will not be any overflows during the sum, and the loop invariant ensures that the sum is correct for the considered sub-array. Notice that the assertion cannot be replaced by a loop invariant, as it should be placed after the assignment to Result and the absence of overflow when adding Result and A (I) could not be proved.

With this implementation, the assertion, the loop invariant and the postcondition are proved. Nevertheless, GNATprove outputs two errors:

acc_def_naive_p.ads:8:13: medium: subprogram "Acc_Def_Rec" might not terminate, terminating annotation could be incorrect
acc_def_naive_p.ads:14:57: medium: overflow check might fail

The first error is simply due to the recursive nature of Acc_Ref_Rec, which is solved with our annotation pragma. The second error makes reference to the line of Acc_Def_Rec where the sum occurs. At this point SPARK cannot prove whether the sum will overflow or not. We therefore need to rewrite our functions to avoid any potential overflow in any part of the code.

A correct version of Accumulate

As mentionned before we need to take care of the overflows in Acc_Def_Rec. Thanks to Claire Dross from AdaCore for the following solution.

Predicates used

To be able to specify that the sums we will compute do not generate any overflow we will first introduce a new option type that contains T values (this type is the same as the Option type defined in Chapter 3, only the type of the encapsulated value changes):

type T_Option (OK : Boolean) is record
   case OK is
      when True =>
	 Value : T;
      when False =>
	 null;
   end case;
end record;

The next function may be the most important of our new version, as it will enable us to verify that no overflow occur:

function Add_No_Overflow
  (X, Y : T)
   return Boolean is
  (Y = 0 or else (Y > 0 and then T'Last - Y >= X)
   or else (Y < 0 and then T'First - Y <= X));

In this function, we verify that the sum of X and Y will not generate an overflow. We cannot check directly the result of X + Y, we only allow operations that do not overflow.

The function checks three cases:

  1. if Y is equal to 0, then no overflow can occur
  2. if Y is strictly positive, then we need to make sure that X + Y is less than T'Last. Mathematically, this is equivalent to verifying that X <= T'Last - Y. It is important to note that this last comparison only contains expressions that will not trigger any overflow.
  3. the same method is applied when Y < 0.

We now have a function that will check if there will be an overflow when adding two values of type T. Acc_Def_Rec and Acc_Def are now rewritten as follows:

function Acc_Def_Rec
  (A    : T_Arr;
   F, L : Integer;
   Init : T)
   return T_Option is
  (if L < F then (True, Init)
   else
     (if
	Acc_Def_Rec (A, F, L - 1, Init).OK
	and then Add_No_Overflow
	  (Acc_Def_Rec (A, F, L - 1, Init).Value, A (L))
      then (True, Acc_Def_Rec (A, F, L - 1, Init).Value + A (L))
      else (OK => False))) with
   Pre => (if L >= F then L in A'Range and F in A'Range);
function Acc_Def
  (A    : T_Arr;
   F, L : Integer;
   Init : T)
   return T_Option is (Acc_Def_Rec (A, F, L, Init)) with
   Pre => (if L >= F then L in A'Range and F in A'Range);

Acc_Def_Rec has been updated to return a T_Option with Value containing the sum of the elements of A from index F to index L, only if no overflow happened during the calculation. Otherwise, the T_Option is be empty.

Notice that the working principle of the algorithm is the same, we simply make sure that there are no overflows in the previous calculations, and that the sum of the result of Acc_Def_Rec (A, F, L - 1, Init) + A (L) does not overflow.

Specification of Accumulate

We can now rewrite the specification for Accumulate:

function Accumulate
  (A    : T_Arr;
   Init : T)
   return T with
   Pre  => (for all J in A'Range => Acc_Def (A, A'First, J, Init).OK),
   Post => Accumulate'Result = Acc_Def (A, A'First, A'Last, Init).Value;

The precondition and postcondition are virtually the same, they simply make use of the new return type of Acc_Def_Rec. We do not need to check that Acc_Def (A, A'First, A'Last, Init).Value exists in the precondition, since this is already ensured by the precondition.

Implementation of Accumulate

An implementation deriving from the previous specification is:

function Accumulate
  (A    : T_Arr;
   Init : T)
   return T
is
   Result : T := Init;
begin
   for J in A'Range loop
      pragma Assert (Acc_Def (A, A'First, J, Init).OK);
      Result := Result + A (J);
      pragma Loop_Invariant (Result = Acc_Def (A, A'First, J, Init).Value);

   end loop;

   return Result;
end Accumulate;

The assertion inside the loop checks that there are no overflow when adding A(J) to the intermediary result. The loop invariant ensures we are doing the right calculations.

With this specification and implementation everything is proved by GNATprove.