RE: [gobo-eiffel-develop] XM_ELEMENT

[Franck A. <fr...@ne...>]

> Franck, it looks like add_attribute() could be useful for enforcing
> well-formedness (unique attribute names).

Well, this use is limited because you can always bypass it by using 
element.force which cannot have a strengthened precondition. This 
could be enforced by an invariant like:

 for_all attributes attribute_is_unique

which can be practically enforced with something like:

 attribute_by_name (attributes.last.name) = attributes.last

(this does not catch everything, but catches a lot. It assumes 
attribute_by_name is speced to return the first attribute 
of the same name, and I'm ignoring namespaces here.)

Besides, I wonder if this restriction is not too strict. While 
strictly speaking not allowed, I had the impression that for 
instance Relax NG may allow duplicate attributes (although 
I couldn't find out for sure when quickly looking at the spec).

--
fr...@ne...