operation FindUser
    inputs: udb:UserDB, id:Id;
    outputs: ur':UserRecord;

    precondition: (* None yet. *);

    postcondition:
        (*
         * If there is a record with the given id in the input db, then the
         * output record is equal to that record, otherwise the output record
         * is empty.
         *);

    description: (*
        Find a user by unique id.
    *);
end FindUser;