operation Add(r:Rolodex, c:Card)->(r':Rolodex)
    precondition: (* The given card is not in the input Rolodex. *);
    postcondition: (* The given card is in the output Rolodex. *);
end Add;