operation AddUser
    inputs: udb:UserDB, ur:UserRecord;
    outputs: udb':UserDB;

    precondition:
        (*
         * There is no user record in the input UserDB with the same id as the
         * record to be added.
         *)
	(not (ur in udb))

            and

        (*
         * The id of the given user record is not empty and 8 characters or
         * less.
         *)
        (#(ur.id) <= 8)

            and

        (*
         * If the phone area code and number are present, they must be 3 digits
         * and 7 digits respectively.
         *)
        (#(ur.phone.area) = 3) and
        (#(ur.phone.num) = 7);


    postcondition: (* Same as above *);

end AddUser;