[review] invariant error in XM_XPOINTER_EVENT_FILTER

The following invariant is wrong regarding the code related to
`attribute_types'

invariant
    attribute_types_not_void: attribute_types /= Void

However the implementation of the creation procedure `make' does not
guarantee `attribute_types' is not Void
Indeed if you check the implementation the `attribute_types' is only set
by feature `set_xpointer', and not by `set_no_filtering'

Suggestion: correct the invariant with the following contracts

    attribute_types_not_void: is_filtering implies attribute_types /= Void

And maybe precise the contract between is_filtering and is_forwarding to
prevent trouble in `on_attribute'
I guess that
        is_forwarding implies is_filtering


Regards,
Jocelyn





------------------------------------------------------------------------------
This SF.net email is sponsored by:
SourcForge Community
SourceForge wants to tell your story.
http://p.sf.net/sfu/sf-spreadtheword