op Find(r:Rolodex, n:Name)->(cl:CardList)
    post:
        CardsFound(r,n,cl)
            and
        SortedById(cl);
end;

function CardsFound(r:Rolodex, n:Name, cl:CardList)->boolean =
    (* Cards in the given card list consist of those in the given Rolodex with
     * the given name *)
    forall (c:Card)
        (c in cl) iff ((c in r) and (c.name = n));

function SortedById(cl:CardList)->boolean =
   (* If the the given card list has more than one card, it is sorted in
    * ascending order by card id. *)
    if (#cl > 1) then
        forall (i:integer | (i >= 1) and (i < #cl))
            cl[i].id < cl[i+1].id;