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