gcc/testsuite/gnat.dg/predicate12.ads

   1 package Predicate12 is
   2
   3    subtype Index_Type is Positive range 1 .. 100;
   4    type Array_Type is array(Index_Type) of Integer;
   5
   6    type Search_Engine is interface;
   7
   8    procedure Search
   9      (S           : in  Search_Engine;
  10       Search_Item : in  Integer;
  11       Items       : in  Array_Type;
  12       Found       : out Boolean;
  13       Result      : out Index_Type) is abstract
  14      with
  15        Pre'Class =>
  16          (for all J in Items'Range =>
  17            (for all K in J + 1 .. Items'Last => Items(J) <= Items(K))),
  18        Post'Class =>
  19          (if Found then Search_Item = Items(Result)
  20                    else (for all J in Items'Range => Items(J) /= Search_Item));
  21
  22    type Binary_Search_Engine is new Search_Engine with null record;
  23
  24    procedure Search
  25      (S           : in  Binary_Search_Engine;
  26       Search_Item : in  Integer;
  27       Items       : in  Array_Type;
  28       Found       : out Boolean;
  29       Result      : out Index_Type) is null;
  30
  31    type Forward_Search_Engine is new Search_Engine with null record;
  32
  33    procedure Search
  34      (S           : in  Forward_Search_Engine;
  35       Search_Item : in  Integer;
  36       Items       : in  Array_Type;
  37       Found       : out Boolean;
  38       Result      : out Index_Type) is null;
  39
  40    procedure Dummy;
  41
  42 end Predicate12;