Set Theory: Examples

Examples of using set theory classes, as specified by st_specification and st_properties, and implemented by st_implementation.

How to use st_specification

Class APPLICATION

The target st_examples_tests of st_examples has a class APPLICATION where are shown examples of how to use classes made upon st_specification and st_implementation libraries.

Class MUTABLE_SET

This class shows how to use st_specification.SET (renamed here to STS_SET) as the specification of a class that models the mathematical concept of a set. It is a simple implementation of STS_SET, i.e. it does only the bare minimum to implement the deferred features of STS_SET. Additionally, it inherits from base.COLLECTION in order to leverage the latter’s features, besides to be used by possible clients of base.CONTAINER and base.ITERABLE. Notice also that MUTABLE_SET does not inherit from st_implementation.SET, since the former’s purpose is to show how to implement STS_SET, whatever the way one prefers to do such an implementation. Other purpose is to show how the “complete” specification of STS_SET, which is “immutable”, eases the specification of features that make in-place changes in MUTABLE_SET objects. Please see the example of {MUTABLE_SET}.intersect’s contract:

        intersect (s: STS_SET [A, EQ])
                        -- Remove all elements not in s.
                ensure
                        intersected: Current ≍ old (Current ∩ s)

Since {STS_SET}.intersected (alias “∩”) already specifies what a set intersection is, turning a (mutable) set into its intersection with another set is rather straightforward.

Class ANNOTATED_ARRAYED_SET

This class shows how to use st_implementation.SET (renamed here to STI_SET) in order to specify the features and invariant of a class like base.ARRAYED_SET. ANNOTATED_ARRAYED_SET inherits from base.ARRAYED_SET and redefines the latter’s features just to add to them set-theory related constraints. A brand-new class may rely directly on STI_SET in order to specify its own features and invariant.

Target st_examples_tests

Please notice that the st_examples_tests target of this project is highly redundant when compared to st_implementation.st_implementation_tests. That is so because the latter is a rather improvised “framework” for testing st_specification, st_properties and st_implementation, so it is not well crafted for reuse “as it is”.