operation FindUser
    inputs: udb:UserDB, id:Id;
    outputs: ur':UserRecord;

    precondition: (* None yet. *);

    postcondition:
        (*
         * If there is a record with the given id in the input db, then the
         * output record is equal to that record, otherwise the output record
         * is empty.
         *)
        (exists (ur in udb) (ur.id = id) and (ur' = ur))
            or
        (not (exists (ur in udb) (ur.id = id)) and (ur' = nil));

    description: (*
        Find a user by unique id.
    *);
end FindUser;

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

    precondition: (* None yet. *);

    postcondition:
        (*
         * A record is in the output list if and only it is in the input UserDB
         * and the record name equals the Name being searched for.
         *)
        (forall (ur: UserRecord)
            (ur in url) iff (ur in udb) and (ur.name = n));

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

operation FindUserByNameAndId
    inputs: udb:UserDB, id:Id, n:Name;
    outputs: ur':UserRecord;

    precondition: (* None yet. *);

    postcondition:
        (*
         * If there is a record with the given name and id in the input db,
         * then the output record is equal to that record, otherwise the output
         * record is empty.
         *)
        (exists (ur in udb) (ur.name = n) and (ur.id = id) and (ur' = ur))
            or
        (not (exists (ur in udb) (ur.name = n) and (ur.id = id)) and (ur' = nil));

    description: (*
        Find a user by both name and id.  This overload of FindUser is
        presumably used infrequently.  Its utility is to confirm that a
        particular user name and id are paired as assumed.
    *);
end FindUserNameAndId;

operation ChangeUser
    inputs: udb:UserDB, old_ur:UserRecord, new_ur:UserRecord;
    outputs:  udb':UserDB;

    precondition: (* None yet. *);

    postcondition:
        (*
         * A user record is in the output db if and only if it is the new
         * record to be added or it is in the input db, and it is not the old
         * record.
         *)
        forall (ur':UserRecord)
            (ur' in udb') iff (((ur' = new_ur) or (ur' in udb)) and
                                   (ur' != old_ur));

    description: (*
        Change the given old UserRecord to the given new record.  The old and
        new records must not be the same.  The old record must already be in
        the input db.  The new record must meet the same conditions as for the
        input to the AddUser operation.  Typically the user runs the FindUser
        operation prior to Change to locate an existing record to be changed.
    *);
end ChangeUser;

operation DeleteUser
    inputs: udb:UserDB, ur:UserRecord;
    outputs: udb':UserDB;

    precondition: (* None yet. *);

    postcondition: 
        (*
         * A user record is in the output db if and only if it is not the
         * existing record to be deleted and it is in the input db.
         *)
        (forall (ur':UserRecord)
            (ur' in udb') iff ((ur' != ur) and (ur' in udb)));

    description: (*
        Delete the given user record from the given UserDB.  The given record
        must already be in the input db.  Typically the user runs the FindUser
        operation prior to Delete to locate an existing record to delete.
    *);
end DeleteUser;