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'.id = ur.id));


    postcondition: (* Same as above *);

end AddUser;