|
Used for OCL Simplification, i.e. not for usual logic terms.
Instead of creating the sorts in this package directly,
use the constants defined in
{@link de.uka.ilkd.key.logic.sort.oclsort.OclSort}.
This package contains representations of the pre-defined types
in OCL: OclAny, OclType, Boolean, Real,
Integer, String.
It also contains means to represent the pre-defined Collection
types: Collection(T), Set(T), Bag(T),
and Sequence(T), where
T is one of the types enumerated above.
Moreover, we need a type that represents the classifiers
defined in the UML model associated with a specific OCL constraint.
We call this representation {@link de.uka.ilkd.key.logic.sort.oclsort.ClassifierSort}.
This sort can be
viewed as a super type of all classifiers in the model.
We don't need more specific type information of the classifiers,
since our simplification rules are based only on our knowledge
of the pre-defined OCL operations - not the properties of a
specific UML model.
Finally, to be able to check for type conformance when building
OCL expressions, we need a sort called
{@link de.uka.ilkd.key.logic.sort.oclsort.OclGenericSort}. Its existence
is motivated in the context of assigning an element type to
an empty Collection. The problem is that when we, for instance,
build an expression like collection->forAll(s:T | e(s))
we want to check that the element type of collection conforms
to the type T. This must hold also for the special case:
Set{}->forAll(s:T | e(s)). In other words, the element type of
Set{} must conform to every other basic type. At the same time,
when we build a collection, we want to check that the types of
the elements in the collection conforms to the element type of
the collection. Using the taclet syntax, $insert_set(elem, $empty_set),
we want to check that the type of elem conforms to the element
type of $empty_set/Set{}. In other words, the element type of
Set{} must be such that any other basic type conforms to it.
We therefore need a type with the property that it conforms to
any other basic type, and any other basic type conforms to it.
{@link de.uka.ilkd.key.logic.sort.oclsort.OclGenericSort} has this property.
Last modified: Thu Jan 27 15:20:36 MET 2005
|