operation Add(r:Rolodex, c:Card)->(r':Rolodex)
    precondition: (* None *);
    postcondition:

        (* The given input card is in the output Rolodex. *)
        c in r'

            and

        (* Any other card is in the output Rolodex
         * only if it is in the input Rolodex *)
        forall (c':Card | c' != c)
            if (c' in r)
            then (c' in r')
            else not (c' in r');
end Add;