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
|
