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