Find_End.org

The Find_End algorithm

The Find_End algorithm finds the last occurence of a given subsquence in a given array. Its signature can be expressed as:

function Find_End (A : T_Arr; B : T_Arr) return Option;

Find_End will return an option containing the greatest valid index I of A such that A (I .. I + B'Length -1 ) = B if it exists.

The Find_End function is quite similar to the Search function, since they both have to find the same thing, the main difference being that Search stops at the first occurence of the subsequence, whereas Find_End will continue looking until finding the last occurence. For this reason, the specification of Find_End will re-use the the ghost functions defined for the specification of Search.

Specification of Find_End

The specification of Find_End is as follows:

function Find_End
  (A : T_Arr;
   B : T_Arr)
   return Option with
   Pre            => A'Last < Positive'Last,
   Contract_Cases =>
   (A'Length >= B'Length and then B'Length /= 0
    and then Has_Subrange (A, B) =>
      Find_End'Result.Exists
      and then Equal_Subrange (A, Find_End'Result.Value, B)
      and then
      (if Find_End'Result.Value < A'Last - B'Length + 1 then
	 (not Has_Subrange (A (Find_End'Result.Value + 1 .. A'Last), B))),
    others => not Find_End'Result.Exists);

• the precondition expresses the fact that the last index of A is less than the last Positive value, as in the ghost functions we will use A'Last+1.
• the postconditions are expressed through 2 contract cases:
  1. if A is longer than B and B is not empty and there is a subsequence in A equal to B (modelled using the Has_Subrange ghost function), then
     • a valid index will be returned
     • the subsequence of A starting at this index and of length B'Length will be equal to B
     • if the returned index is not A'Last - B'Length + 1 (the last index where a subsequence of A can be equal to B), then for all indexes K of A greater than the returned index, the subsequence of length B'Length starting at index K is not equal to B.
  2. otherwise there is no index returned.

Implementation of Find_End

function Find_End
  (A : T_Arr;
   B : T_Arr)
   return Option
is
   Result : Option := (Exists => False);
begin
   if (A'Length < B'Length or else B'Length = 0) then
      return Result;
   end if;

   for J in A'First .. A'Last - B'Length + 1 loop
      if A (J .. J - 1 + B'Length) = B then
	 Result := (Exists => True, Value => J);

	 pragma Assert (J - 1 + B'Length = Last (J, B));
      end if;

      pragma Loop_Invariant
	(if Result.Exists then
	   Has_Subrange (A, B)
	   and then Result.Value in A'First .. A'Last + 1 - B'Length
	   and then Equal_Subrange (A, Result.Value, B)
	   and then
	   (if Result.Value < J then
	      not Has_Subrange
		(A (Result.Value + 1 .. J - 1 + B'Length), B))
	 else not Has_Subrange (A (A'First .. J - 1 + B'Length), B));

   end loop;

   return Result;

end Find_End;

• the implementation is rather simple: we range over A indexes trying to find a subsequence equal to B, each time we do find one we save the current index J in Result.Value. Contrary to Search, we do not return at the first match since we want to find the last subsequence of A equal to B. We examine instead the entire range of indexes.
• the loop invariant specifies that:
  1. either Result.Exists is true and then:
     • there is a subsequence of A equal to B
     • Result.Value is in the range A'First .. A'Last - B'Length + 1
     • the subsequence of A of length B'Length starting at Result.Value is equal to B
     • If Result.Value is different from J then for all K in Result'Value+1 .. J there is no subrange of A starting at index K of length B'Length equal to B
  2. or no matching subsequence of A starting at an index lower than J has been found.

Notice that in order to prove the loop invariant on Has_Subrange we must add an assertion when finding a correct index to help the solvers by identifying J - 1 + B'Length with Last (J, B).

Using GNATprove on Find_End, all the assertions are proved.