operation Add(r:Rolodex, c:Card)->(r':Rolodex)
    precondition: 
        (* There is no card in the input Rolodex with the same Id
         * as the given input card. *)
        not (exists (c' in r) c'.id = c.id);

    postcondition: (* Same as above *);
end Add;