operation FindUser
    inputs: udb:UserDB, n:Name;
    outputs: url:UserRecord*;

    precondition: (* None yet. *);

    postcondition:
        (*
         * The output list consists of all records of the given name in the
         * input db.
         *)
        (forall (ur: UserRecord) (ur in url) iff (ur in udb) and (ur.name = n))

            and

        (*
         * The output list is sorted alphabetically by id.
         *)
        (forall (i:integer | (i >= 1) and (i < #url))
            url[i].id < url[i+1].id);

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