Skip to content

Latest commit

 

History

History
111 lines (87 loc) · 3.34 KB

Adjacent_Difference.org

File metadata and controls

111 lines (87 loc) · 3.34 KB

The Adjacent_Difference algorithm

The Adjacent_Difference algorithm will compute for each index J of an array A the difference between the value at index J and the value at index J - 1. The results are stored in another array B. Its signature is the following:

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

Predicate used

To be able to properly specify this algorithm, we need to write an overflow verification function for substractions. One could argue that using the function Add_No_Overflow defined for function Accumulate with a minus sign in front of the second argument is sufficient, but our function must work with the entire range of T, which is the entire range of Ada Integer. There is therefore one case in which executing - Y triggers an overflow, since there is one more negative value in Integer than positive values.

The function Minus_No_Overflow is defined as follows:

function Minus_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));

Of course, this function is implemented and specified like Add_No_Overflow.

Specification of Adjacent_Difference

We can now give a specification for Adjacent_Difference:

procedure Adjacent_Difference
  (A :        T_Arr;
   B : in out T_Arr) with
   Pre =>
   (if A'Length > 0 then
      (for all J in A'First + 1 .. A'Last =>
	 Minus_No_Overflow (A (J), A (J - 1))))
   and then B'Length = A'Length,
   Post =>
   (if A'Length > 0 then
      B (B'First) = A (A'First)
      and then
      (for all J in A'First + 1 .. A'Last =>
	 B (B'First + J - A'First) = A (J) - A (J - 1)));

The precondition states that there should be no overflow when subtracting any value to the one following, and that both arrays should be of same length.

The postcondition ensures that the first elements of both arrays are equal, and that each element of B is the result of the subtraction of the corresponding element and the previous one in A.

Implementation of Adjacent_Difference

We can write an implementation for the procedure respecting the previous specification easily:

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

      if A'Length = 1 then
	 return;
      end if;
      for J in A'First + 1 .. A'Last loop

	 pragma Assert (Minus_No_Overflow (A (J), A (J - 1)));

	 B (J - A'First + B'First) := A (J) - A (J - 1);

	 pragma Loop_Invariant
	   (for all K in A'First + 1 .. J =>
	      B (B'First + K - A'First) = A (+K) - A (K - 1));
	 pragma Loop_Invariant (B (B'First) = A (A'First));

      end loop;

   end if;
end Adjacent_Difference;

The algorithm is really simple. There is only one assertion inside the loop to check that there is no overflow when computing the difference of A (J) and A (J - 1). The loop invariants verify that we are doing the correct calculation, and that the first index of B is constant.

This implementation is proved by GNATprove.