op Find(r:Rolodex, n:Name)->(c:Card)
    pre:
        (* There is a card in the given Rolodex
         * with the given name. *)
        exists (c' in r) c'.name = n;
    post: 
        (* The output card is in the given Rolodex
         * and has the given name. *)
        (c in r) and (c.name = n);
end;