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

    postcondition:
        (*
         * A user record is in the output db if and only if it is the new
         * record to be added or it is in the input db.
         *)
        forall (ur':UserRecord)
            (ur' in udb') iff ((ur' = ur) or (ur' in udb));

end AddUser;