Re: [review] invariant error in XM_XPOINTER_EVENT_FILTER

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:[email protected]
http://www.gobosoft.com

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