The goal of this library is to provide a complete specification of set theory concepts, but keeping it open for any possible implementation. The reason for such a design decision is that an implementation of the specified classes may be vastly different depending of the purpose of the implementation. For example, if implemented in order to produce classes to be used as models for specifications (like MML), the resulting implementation might be significantly different from another implementation whose scope is to provide structures for general data manipulation.
Eiffel has its own quantifiers, e.g. ∃ c: s ¦ some_condition (c). But they require that s be a descendant of ITERABLE, and a key idea of st_specification is to rely as least as possible upon EiffelBase or any other library, since it should be able to annotate and model those libraries. Hence the somewhat awkward syntax of st_specification quantifiers, since they cannot benefit from Eiffel iteration mechanism.
Many features within
st_specification
exist only to be used within agents (although they can be used by
their own, of course). The need for such features lies in the fact
that the Contract view of EiffelStudio does not show the body of
inline agents. Hence e.g. the post-condition clause of {SET}.united
whose tag is nothing_else
cannot read
Result
|∀ agent (ia_s: STS_SET [A, EQ]; ia_x: A): BOOLEAN
do
Result
:= Current ∋ ia_x or ia_s ∋ ia_x
end (s, ?)
as
would be more straightforward.
#19883: In Project Settings → Target node, the options below Language section are not saved.