operation Add(r:Rolodex, c:Card)->(r':Rolodex)
    precondition:
        (#(c.name) <= 30)  (* The length of the name is <= 30 characters *)
            and
        (#(c.id) = 9)  (* The length (i.e, number of digits) of the id is 9 *)
            and
        ((c.age >= 0) and (c.age <= 200))  (* Age is a reasonable range *)
            and
        (#(c.addr) < 40)  (* The length of the address is <= 40 chars *)

        and not (exists (c' in r) c'.id = c.id); (* No dups condition from above *)

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