| java.lang.Object
 de.uka.ilkd.key.logic.sort.AbstractSort
de.uka.ilkd.key.logic.sort.IntersectionSort
| IntersectionSort | | public class IntersectionSort extends AbstractSort (Code) | |
An intersection sort I is composed by exactly two sorts S,
T and denotes their maximal subsort. This means, each sort being a subsort
of both components extends (or is equal to) I as well.
An intersection sort is always normalized during creation in order to keep consistent
with the singleton property of sorts. That is to say that creation of the intersection
sort (S,T) and (T,S), which denote obviously the same sort, returns the same sort object
as they have the same normalform.
The normalform is defined as follows:
- (S1,S2),
where S1 must be a simple (non-intersection) sort; for
S2 there is no such restriction
- S1 is no subsort of S2 and vice versa,
i.e. intersection sorts are minimized
- (S1,S2) are lexicographical ordered such that the name of S1
is smaller than the name of sort S2 (if S2 is a simple sort)
or otherwise smaller than any sort being a composite of sort S2
If the normalform consists of exact one sort than the creation method of intersection
sort returns the sort itself.
An alternative definition of a normalform may use flattening, but
would make matching of taclets more difficult.
|
| extendsSorts | | public SetOfSort extendsSorts()(Code) | | return the set of the 'real' sorts this
intersection sort consists of (no intersection sorts)
|
| extendsTrans | | public boolean extendsTrans(Sort p_sort)(Code) | | returns true iff the given sort is a transitive supersort of this sort
or it is the same.
|
| getComponent | | public Sort getComponent(int i)(Code) | | returns the i-th component of this intersection sort
(where 0 is left component and 1 is the right component)
the i-th component of this intersection sort
throws:
IndexOutOfBoundsException - if i is greater than 1 |
| getIntersectionSort | | public static Sort getIntersectionSort(SetOfSort sorts, Services services)(Code) | | performs a lookup in the sort namespace and returns the
intersection sort of the given sorts. If none exists a new
intersection sort is created and added to the namespace.
The created intersection sort is in normalform.
Parameters:
sorts - the SetOfSort whose intersection sort has to be determined
Parameters:
services - the Namespace with all known sorts to which if necessary the intersection sort of the given sorts is added the intersection sort of the given sorts. |
| getIntersectionSort | | public static Sort getIntersectionSort(SetOfSort components, Namespace sorts, Namespace functions)(Code) | | performs a lookup in the sort namespace and returns the
intersection sort of the given sorts. If none exists a new
intersection sort is created and added to the namespace.
The created intersection sort is in normalform.
Parameters:
components - the SetOfSort whose intersection sort has to be determined
Parameters:
sorts - the Namespace with all known sorts to which if necessary the intersection sort of the given sorts is added
Parameters:
functions - the Namespace where to add the sort depending functions the intersection sort of the given sorts. |
| getIntersectionSort | | public static Sort getIntersectionSort(Sort s1, Sort s2, Namespace sorts, Namespace functions)(Code) | | performs a lookup in the sort namespace and returns the
intersection sort of the given sorts. If none exists a new
intersection sort is created and added to the namespace.
The created intersection sort is in normalform.
Parameters:
s1 - the first Sort
Parameters:
s2 - the second Sort
Parameters:
sorts - the Namespace with all known sorts to which if necessary the intersection sort of the given sorts is added
Parameters:
functions - the Namespace where to add sort depending functions like instance, casts etc. the intersection sort of the given sorts. |
| hasEmptyDomain | | public boolean hasEmptyDomain()(Code) | | returns true if the represented domain is empty. If you consider other logics
than JavaCardDL you will most probably have to subclass IntersectionSort and
overwrite this method.
true if other than reference types, which are siblings in the type hierarchy, intersect |
| memberCount | | public int memberCount()(Code) | | returns the number of composites (always two)
|
|
|