Partial_Sum.org

The Partial_Sum algorithm

The Partial_Sum algorithm computes the consecutive partial sums of an array. Its signature reads:

procedure Partial_Sum (A : T_Arr; B : in out T_Arr);

The result of the algorithm will be stored in B, and for all K in (0 .. A'Length - 1), B (B'First + K) = A (A'First) + A (A'First + 1) + .. + A (A'First + K). This can also be expressed with the previously defined Accumulate algorithm: for all K in 0 .. A'Length-1 then B (B'First + K) = Accumulate (A (A'First .. A'First + K), 0).

Specification of Partial_Sum

Partial sum can be specified as follows:

procedure Partial_Sum
  (A :        T_Arr;
   B : in out T_Arr) with
   Pre => A'Length = B'Length
   and then (for all J in A'Range => Acc_Def (A, A'First, J, 0).OK),
   Post =>
   (for all J in A'Range =>
      B (B'First + (J - A'First)) = Acc_Def (A, A'First, J, 0).Value);

The preconditions express that A and B must be of same length, and that there should be no overflows during the computation of the sum. The postcondition expresses the fact that the element found at index J in B is equal to the sum of the J first elements of A.

Implementation of Partial_Sum

Given its specification, Partial_Sum can be implemented as follows:

procedure Partial_Sum
  (A :        T_Arr;
   B : in out T_Arr)
is
begin
   if A'Length > 0 then
      B (B'First) := A (A'First);

      for J in 1 .. A'Length - 1 loop

	 pragma Assert (Acc_Def (A, A'First, A'First + J, 0).OK);
	 pragma Assert
	   (Add_No_Overflow (A (A'First + J), B (B'First + (J - 1))));
	 B (B'First + J) := B (B'First + (J - 1)) + A (A'First + J);

	 pragma Loop_Invariant
	   (for all K in 0 .. J =>
	      B (B'First + K) = Acc_Def (A, A'First, A'First + K, 0).Value);

      end loop;
   end if;
end Partial_Sum;

This implementation is quite similar to the one of Accumulate, the assertions ensures that there are no overflows and the loop invariant verifies that the computed values are correct.

With this implementation and specification, everything is proved by GNATprove.