object SearchInfo =  np:NamePattern and idp:IdPattern and 
        ap:AgePattern and sp:SexPattern and adp:AddressPattern
    description: (*
        Each component of SearchInfo is a search pattern that corresponds to
        one of the fields of a card.
    *);
end SearchInfo;

obj NamePattern =   ...;
obj IdPattern =   ...;

object AgePattern =  lessp:AgeLessThan or gtrp:AgeGreaterThan or
        rangep:AgeRange or eqp:Age
    description: (*
        An AgePattern allows the user to search for cards with an age value
        less than a given age, greater than a given age, between a range of
        given ages, equal to a specific age, or with a specific age.
    *);
end AgePattern;

obj SexPattern =  ...;
obj AddressPattern =  ...;

object AgeLessThan =  lts:LessThanSymbol and age:Age
    description: (*
        This pattern specifies all ages less than a particular age.
    *);
end AgeLessThan;

object AgeGreaterThan =  lts:GreaterThanSymbol and age:Age
    description: (*
        This pattern specifies all ages greater than a particular age.
    *);
end AgeGreaterThan;

object AgeRange =  age1:Age and rs:RangeSymbol and age2:Age
    description: (*
        This pattern specifies all ages in a range between age1 and age2.
    *);
end AgeRange;

object LessThanSymbol;
object GreaterThanSymbol;
object RangeSymbol;

operation Find (r:Rolodex, si:SearchInfo)->(cl:Card*)
    pre:  ... ;
    post:
        (* 
         * All cards in the output list must be found according to the given
         * search info, and the output list must be sorted by Card id.
         *)
        CardsFound(r,si,cl)
            and
        SortedById(cl);
    description: (*
        Find zero or more cards that match the constraints specified in the
        given SearchInfo. 
    *);
end Find;

function CardsFound(r:Rolodex, si:SearchInfo, cl:Card*)->boolean =
    (* Cards in the given card list consist of those, and only those, in the
     * given Rolodex that match the given search info. *)
    forall (c:Card)
        (c in cl) iff ((c in r) and Match(c,si));

function Match(c:Card, si:SearchInfo)->boolean =
        MatchName(c.name, si.np) and
        MatchId(c.id, si.idp) and
        MatchAge(c.age, si.ap) and
        MatchSex(c.sex, si.sp) and
        MatchAddress(c.addr, si.adp);

function MatchName(Name, NamePattern)->boolean =  ... ;
function MatchId(Id, Idpattern)->boolean =  ... ;

function MatchAge(age:Age, ap:AgePattern)->boolean =
    if (ap?.lessp) then
        age < ap.lessp.age
    else if (ap?.gtrp) then
        age > ap.gtrp.age
    else if (ap?.rangep) then
        (age >= ap.rangep.age1) and (age <= ap.rangep.age2)
    else if (ap?.eqp) then
        age = ap.eqp.age
    else if (ap = nil) then
        true;

function MatchSex(Sex, SexPattern)->boolean = ... ;
function MatchAddress(Address, AddressPattern)->boolean =  ...;