Skip to content

Latest commit

 

History

History
123 lines (99 loc) · 3.65 KB

Count.org

File metadata and controls

123 lines (99 loc) · 3.65 KB
Raw

The Count algorithm

The Count algorithm counts the number of occurrences of a value Val in an array A. Its signature can be expressed as:

function Count (A : T_Arr; Val : T) return Natural;

The predicate Occ

We want to define a ghost function Occ returning the number of occurences of a given value in an array. This ghost function will serve as a mathematical specification for Count.

Occ can classically be defined recursively on the length of the array (see SPARK 2014 user guide chapter on manual proof with ghost code for a similar and more detailed example). We first define a recursive function Occ_Def which will be used in Occ as GNATprove only introduces axioms for postconditions of non-recursive functions.

function Remove_Last
  (A : T_Arr)
   return T_Arr is (A (A'First .. A'Last - 1)) with
   Pre => A'Length > 0,
   Ghost;

function Occ_Def
  (A   : T_Arr;
   Val : T)
   return Natural is
  (if A'Length = 0 then 0
   elsif A (A'Last) = Val then Occ_Def (Remove_Last (A), Val) + 1
   else Occ_Def (Remove_Last (A), Val)) with
   Post => Occ_Def'Result <= A'Length;
pragma Annotate (Gnatprove, Terminating, Occ_Def);

The line pragma Annotate (Gnatprove, Terminating, Occ_Def); is very important here. It states that the function Occ_Def terminates. Without this annotation, the tool would not be able to prove some loop invariants. In return, GNATprove prints medium: subprogram "Occ_Def" might not terminate, terminating annotation could be incorrect indicating that the user should verify by other means that Occ_Def really terminates.

After having defined Occ_def, the definition of Occ is rather easy:

function Occ
  (A   : T_Arr;
   Val : T)
   return Natural is (Occ_Def (A, Val)) with
   Post => Occ'Result <= A'Length;
function Occ (A : T_Arr; Val : T) return Natural is (Occ_Def (A, Val)) with
  Post => Occ'Result <= A'Length;

The postcondition is necessary to prove loop invariants in Count.

Specification of Count

The specification of Count is the following:

function Count
  (A   : T_Arr;
   Val : T)
   return Natural with
   Post =>
   (Count'Result <= A'Length and then Count'Result in 0 .. A'Length
    and then Count'Result = Occ (A, Val));

The postconditions express

  • that the number returned is correct (it is not less than 0 nor is it more than A'Length).
  • that the number returned is equal to the number of occurrences of Val in the array A.

Implementation of Count

The implementation of Count is the following:

function Count
  (A   : T_Arr;
   Val : T)
   return Natural
is
   Result : Natural := 0;
begin
   for I in A'Range loop
      if A (I) = Val then
	 Result := Result + 1;
      end if;

      pragma Loop_Invariant (Result <= A'Length);
      pragma Loop_Invariant (Result = Occ (A (A'First .. I), Val));
   end loop;

   return Result;
end Count;

The first invariant states that Result always stays in a correct range. The second one states that at each loop iteration, we can assert that Result is equal to the number of occurrences of Val in the slice of the array that has currently been traversed.

When using GNATprove on Count everything is proved (except the termination of Occ_Def).