op Delete(r:Rolodex, n:Name)->(r':Rolodex)
    pre: ;
    post:
        (* Cards in the output Rolodex consist of those
         * in the input Rolodex, except for those with
         * the same name as the given input name. *)
        forall (c':Card)
            (c' in r') iff ((c' in r) and (c'.name != n));
end;

op Change(r:Rolodex, n:Name, c:Card)->(r':Rolodex)
    pre: ;
    post:
        (* The given card is in the output Rolodex *)
        (c in r')

            and

        (* No other cards of the same name are in the Rolodex *)
        forall (c':Card | c' != c)
            (c' in r') iff ((c' in r) and (c'.name != n));
end;