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_______________________________________________
gobo-eiffel-develop mailing list
[hidden email]
https://lists.sourceforge.net/lists/listinfo/gobo-eiffel-develop
