Re: [gobo-eiffel-develop] [review] invariant error in XM_XPOINTER_EVENT_FILTER

[Eric B. <er...@go...>]

Jocelyn wrote:
> 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

Done. I also reset `attribute_types' to Void in `set_no_filtering'.

> 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

I don't see where the trouble is in `on_attribute'.

-- 
Eric Bezault
mailto:er...@go...
http://www.gobosoft.com