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 (exists (ur' in udb) ur = ur))

            and

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

            and

        (*
         * The email address is not empty.
         *)
        (ur.email != nil)

            and

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


    postcondition: (* Same as above *);

end AddUser;