operation FindUserByName
    inputs: udb:UserDB, name:Name;
    outputs: ur':UserRecord*;

    precondition: (* None yet. *);

    postcondition:
        (*
         * A record is in the output list if and only if it is in
         * the input UserDB and the record name equals the Name
         * being searched for
         *);

    description: (*
        Find a user or users by real-world name. If more than one is
        found, output list is sorted by id.
    *);
end FindUserByName;