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

    postcondition:
        RecordsFound(udb,n,url)
            and
        SortedById(url);

end FindUserByName;

function RecordsFound(udb:UserDB, n:Name, url:UserRecord*) =
    (*
     * The output list consists of all records of the given name in the input
     * db.
     *)
    (forall (ur' in url)
       (ur' in udb)
          and
       (ur'.name = n));

function SortedById(url:UserRecord*) =
    (*
     * The output list is sorted alphabetically by id.
     *)
        (if (#url > 1) then
            (forall (i in [1..(#url - 1)])
               url[i].id < url[i+1].id)
         else true);