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

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

end FindUser;

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.
     *)
    (forall (i:integer | (i >= 1) and (i < #url))
        url[i].id < url[i+1].id);