blob: f51e649e9f786685406fb6a91bd4f6242fb8e9d9 [file] [log] [blame]
package Predicate12 is
subtype Index_Type is Positive range 1 .. 100;
type Array_Type is array(Index_Type) of Integer;
type Search_Engine is interface;
procedure Search
(S : in Search_Engine;
Search_Item : in Integer;
Items : in Array_Type;
Found : out Boolean;
Result : out Index_Type) is abstract
with
Pre'Class =>
(for all J in Items'Range =>
(for all K in J + 1 .. Items'Last => Items(J) <= Items(K))),
Post'Class =>
(if Found then Search_Item = Items(Result)
else (for all J in Items'Range => Items(J) /= Search_Item));
type Binary_Search_Engine is new Search_Engine with null record;
procedure Search
(S : in Binary_Search_Engine;
Search_Item : in Integer;
Items : in Array_Type;
Found : out Boolean;
Result : out Index_Type) is null;
type Forward_Search_Engine is new Search_Engine with null record;
procedure Search
(S : in Forward_Search_Engine;
Search_Item : in Integer;
Items : in Array_Type;
Found : out Boolean;
Result : out Index_Type) is null;
procedure Dummy;
end Predicate12;