operation AddUser
    inputs: UserDB, UserRecord;
    outputs: UserDB;
    precondition: (* Coming soon *);
    postcondition: (* Coming soon *);
    description: (*
        Add the given UserRecord to the given UserDB.  The Id of the given user
        record must not be the same as a user record already in the UserDB.
        The Id component is required and must be eight characters or less.  The
        email address is required.  The phone number is optional; if given, the
        area code and number must be 3 and 7 digits respectively.
    *);
end;

operation FindUser
    inputs: UserDB, Id;
    outputs: UserRecord;
    precondition: (* Coming soon *);
    postcondition: (* Coming soon *);
    description: (*
        Find a user by unique id.
    *);
end;

operation FindUser
    inputs: UserDB, Name;
    outputs: UserRecord;
    precondition: (* Coming soon *);
    postcondition: (* Coming soon *);
    description: (*
        Find a user or users by real-world name.  If more than one is found,
        output list is sorted by id.
    *);
end;

operation FindUser
    inputs: UserDB, Id, Name;
    outputs: UserRecord;
    precondition: (* Coming soon *);
    postcondition: (* Coming soon *);
    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;

operation ChangeUser
    inputs: UserDB, UserRecord, UserRecord;
    outputs:  UserDB;
    precondition: (* Coming soon *);
    postcondition: (* Coming soon *);
    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;

operation DeleteUser
    inputs: UserDB, UserRecord;
    outputs: UserDB;
    precondition: (* Coming soon *);
    postcondition: (* Coming soon *);
    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;