Re: module Set

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>]

> Abstract data types have a specification and an implementation.
> The specification usually does not specify everything about the
> behavior of the implementation, if only to allow the implementation to
> change later without breaking user's code.
> 
> In the case of Set, the ordering property you see is a consequence of
> the implementation of sets as search trees.  But other implementations
> (e.g. using hashing) would break that property.

I perfectly agree. But I didn't ask for an interface specifying that
the implementation is based on AVL;  I was just asking for an interface
saying that the elements returned by "elements" are sorted. And it is
always possible to write such a function since the type of elements is
ordered (Independently from the implementation, it is always possible
to sort the lists of the elements of the set before returning it). 
The abstraction of the module Set is not endangered by this additional
property.

-- 
Jean-Christophe FILLIATRE
  mailto:Jean-Christophe.Filliatre@lri.fr
  http://www.lri.fr/~filliatr