Skip to content

Latest commit

 

History

History
202 lines (163 loc) · 6.94 KB

Numeric_Inv.org

File metadata and controls

202 lines (163 loc) · 6.94 KB

Inverting Partial_Sum and Adjacent_Difference

With our specifications for Partial_Sum and Adjacent_Difference, we can easily show that calling them one after the other in the following way:

Partial_Sum (A, B);
Adjacent_Difference (B, A);

or

Adjacent_Difference (A, B);
Partial_Sum (B, A);

will leave A unchanged. But as we have proved these functions with SPARK, we can also prove these properties with SPARK.

Inverting Partial_Sum with Adjacent_Difference

We will first show that we can invert Partial_Sum with Adjacent_Difference. In order to prove this, we write a procedure with a unique postcondition, being that our input array is left unmodified, and that should only call Partial_Sum and Adjacent_Difference in its implementation. Its signature is:

Partial_Sum_Inv (A, B : in out T_Arr);

Specification of Partial_Sum_Inv

Partial_Sum_Inv can be specified in the following way:

procedure Partial_Sum_Inv (A, 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 => A = A'Old;

The preconditions are the same than the preconditions of Partial_Sum. The postcondition expresses the fact that A should remain unchanged.

Implementation of Partial_Sum_Inv

Our implementation of Partial_Sum_Inv is the following:

procedure Partial_Sum_Inv (A, B : in out T_Arr) is
   Init : T_Arr := A with
      Ghost;  -- not used anywhere, but somehow helps prove the loop invariants.
begin
   if A'Length = 0 then
      return;
   end if;

   Partial_Sum (A, B);
   pragma Assert (A (A'First) = B (B'First));

   if A'Length > 1 then
      pragma Assert
	(for all J in B'First + 1 .. B'Last =>
	   B (J) = B (J - 1) + A (A'First + (J - B'First)));
      pragma Assert
	(for all J in A'First + 1 .. A'Last =>
	   A (J) =
	   B (B'First + (J - A'First)) - B (B'First + (J - 1 - A'First)));
   end if;

   Adjacent_Difference (B, A);
end Partial_Sum_Inv;

We simply assert here that if the length of A is greater or equal to 1 (nothing needs to be proven otherwise) then after calling Partial_Sum the preconditions of Adjacent_Difference are respected. We exhibit a relation between B (J) and B (J - 1), which then enables the solvers to prove the precondition. The relation between the elements of B in the assertion also enables the solvers to prove that Adjacent_Difference does return A to its original state.

Inverting Adjacent_Difference with Partial_Sum

The methodology is the same as the previous one.. The signature of the function representing the property is:

procedure Adjacent_Difference_Inv (A, B : in out T_Arr)

Specification of Adjacent_Difference_Inv

Adjacent_Difference_Inv can be specified in the following way:

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

The preconditions are those of Adjacent_Difference. The postcondition once again ensures that A remains unmodified.

Implementation of Adjacent_Difference_Inv

The implementation of Adjacent_Difference_Inv is the following:

procedure Adjacent_Difference_Inv (A, B : in out T_Arr) is
   Tmp : T with
      Ghost;
begin
   if A'Length = 0 then
      return;
   end if;
   Tmp := A (A'First);
   Adjacent_Difference (A, B);
   pragma Assert
     (Acc_Def (B, B'First, B'First, 0).OK
      and then Acc_Def (B, B'First, B'First, 0).Value = Tmp);

   if A'Length > 1 then
      for J in A'First + 1 .. A'Last loop

	 pragma Assert (B (J - A'First + B'First) = A (J) - Tmp);

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

	 pragma Loop_Invariant (Tmp = A (J));
	 pragma Loop_Invariant
	   (for all K in A'First .. J =>
	      Acc_Def (B, B'First, K - A'First + B'First, 0).OK
	      and then
		Acc_Def (B, B'First, K - A'First + B'First, 0).Value =
		A (K));
	 pragma Loop_Invariant
	   (for all K in B'First .. J - A'First + B'First =>
	      Acc_Def (B, B'First, K, 0).OK);
      end loop;
   end if;
   Partial_Sum (B, A);

end Adjacent_Difference_Inv;

There are more things to annotate in this function, because the preconditions of Partial_Sum are more constraining than the ones of Adjacent difference. In order to prove the preconditions of Partial_Sum, we use a ghost variable, Tmp, which computes the partial sums of B inside the loop. As we can annotate the loop with loop invariants, we can verify that in each iteration that there is a relation between the elements of B, the elements of A and Tmp. This ensures that there is no overflow when computing the next partial sum, and the relations found help prove that A will return to its initial state after executing Partial_Sort(B,A).

There is one important thing that needs to be pointed out in this code. The second loop invariant mathematically implies the third, as the main difference is the range used for the quantified variable K. In the second loop_invariant K ranges over indexes of A whereas in the third loop invariant K ranges over indexes of B. Both are proved just fine, but if we only keep the second loop invariant then the preconditions of Partial_Sum are not verified, and if we only keep the third (and we add the relation between A and Acc_Def(B ...)), then the postcondition is not verified.

This is due to a limitation of automatic solvers on arithmetic with universally quantified assertions. If we look at the preconditions of Partial_Sum we can see that the quantified variable J is in A'Range and that we verify that Acc_Def (A, A'First, J, 0).OK holds. When trying to verify this precondition, the solvers will range over the previous assertions with a universally quantified variable to try to match the precondition, but all the assertions in our invariants are in the form of Acc_Def (B, B'First, J - A'First + B'First, 0), which cannot be matched with the quantified variable. That is why adding the third loop invariant, which seems to prove what was already proven by the second loop invariant, is not redundant. Proving the equality of the arrays has the same issue, because proving that A = A'Old is equivalent to proving that for all J in A'Range => A(J) = A'Old(J), and ranging over the indexes of B would introduces the same issues if we only keep the third invariant.

GNATprove proves that this implementation is correct with respect to the specification. We have therefore proved the desired property.