1package 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 42end Predicate12; 43