Skip to content

Latest commit

 

History

History
126 lines (98 loc) · 3.72 KB

Min_Element.org

File metadata and controls

126 lines (98 loc) · 3.72 KB

The Min_Element algorithm

The Min_Element algorithm searches the minimum in a general sequence. Its signature can be expressed as:

function Min_Element(A : T_arr) return Option;

Min_Element will return an option containing the first index I of A such as for all K in A'First .. A'Last, A(I) <= A(K). It is of course an algorithm very similar to Max_Element.

Predicates used for specification

As for Max_Element, we will first define predicates to help readability of specification.

The Lower_Bound predicate

The Lower_Bound predicate will be used to assert that the return value is a lower bound for the values of A (A'First .. N), where N is given:

function Lower_Bound
  (A : T_Arr;
   V : T)
   return Boolean is (for all I in A'First .. A'Last => A (I) >= V);

The Strict_Lower_Bound predicate

The Strict_Lower_Bound predicate will be used to confirm that the returned value is the first valid index for a minimum. It expresses the fact that all the values of A before index N are strictly lesser than V:

function Strict_Lower_Bound
  (A : T_Arr;
   V : T)
   return Boolean is (for all I in A'First .. A'Last => A (I) > V);

The Specification of Min_Element

The specification of Min_Element can be expressed as follows:

function Min_Element
  (A : T_Arr)
   return Option with
   Contract_Cases => (A'Length = 0 => not Min_Element'Result.Exists,
    A'Length > 0 =>
      Min_Element'Result.Exists and then Min_Element'Result.Value <= A'Last
      and then Min_Element'Result.Value >= A'First
      and then Lower_Bound (A, A (Min_Element'Result.Value))
      and then
      (if Min_Element'Result.Value > A'First then
	 Strict_Lower_Bound
	   (A (A'First .. Min_Element'Result.Value - 1),
	    A (Min_Element'Result.Value))));

Here, the postconditions are expressed through 2 contract cases:

  • if A is empty then an “empty” Option is returned
  • else there is a valid index returned and
    1. the result is a lower bound for the values in A
    2. for all value V of A found at an index stricly lower than Result.Value then V > A(Result.Value). This expresses the fact that the result is indeed the first index containing the minimum element of A.

Implementation of Min_Element

function Min_Element
  (A : T_Arr)
   return Option
is
   Result : Option := (Exists => False);
begin
   if A'Length = 0 then
      return Result;
   else
      Result := (Exists => True, Value => A'First);

      for I in A'First .. A'Last loop
	 if A (I) < A (Result.Value) then
	    Result.Value := I;
	 end if;

	 pragma Loop_Invariant (Result.Value in A'First .. A'Last);
	 pragma Loop_Invariant
	   (Lower_Bound (A (A'First .. I), A (Result.Value)));
	 pragma Loop_Invariant
	   ((if Result.Value > A'First then
	       Strict_Lower_Bound
		 (A (A'First .. Result.Value - 1), A (Result.Value))));

      end loop;

      return Result;

   end if;

end Min_Element;

The implementation is quite similar to the one of Max_Element with predicates. Here the loop invariants specify that

  1. the result is in a valid range
  2. the current result is a minimum for all the values already examined (from A'First to I)
  3. the current minimum is the first occurrence of this value in A (i.e. all previous values of A are striclty greater)

When using GNATprove on this specification and implementation, everything is proved.