op Find(r:Rolodex, n:Name)->(cl:CardList)
    post:

        (* Cards in the output list consist of those in the input Rolodex with
         * the given name. *)
        forall (c:Card)
            (c in cl) iff ((c in r) and (c.name = n))

            and

        (* The output card list is sorted in ascending order by card id. *)
        forall (i:integer | (i >= 1) and (i < #cl))
            cl[i].id < cl[i+1].id;
end;