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. If the list has more
         * than one record, make sure it's sorted. A list with one record is,
         * by default, sorted.
         *)
        (if (#url > 1) then
            (forall (i in [1..(#url - 1)])
               url[i].id < url[i+1].id)
         else true);

    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;

(*
 * Create some testing values.
 *)
val ur1:UserRecord = {"Corwin", "1", nil, nil};
val ur2:UserRecord = {"Fisher", "2", nil, nil};
val ur3:UserRecord = {"Other", "3", nil, nil};
val ur4:UserRecord = {"Extra", "4", nil, nil};
val ur5:UserRecord = {"Fisher", "5", nil, nil};

val udb = [ur1, ur2, ur3, ur4, ur5];
val unsorted_result = [ur5, ur3];
val sorted_result = [ur3, ur5];

> "Expected results of FindUser(udb,''Fisher'')?->unsorted_result are { true, false }:";
> FindUser(udb,"Fisher")?->unsorted_result;