| java.lang.Object de.uka.ilkd.key.logic.sort.AbstractSort de.uka.ilkd.key.logic.sort.AbstractNonCollectionSort de.uka.ilkd.key.logic.sort.GenericSort
GenericSort | public class GenericSort extends AbstractNonCollectionSort implements ObjectSort(Code) | | Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
Field Summary | |
SetOfSort | ext | SetOfSort | oneOf |
Constructor Summary | |
public | GenericSort(Name name) | public | GenericSort(Name name, SetOfSort ext, SetOfSort oneOf) creates a generic sort
Parameters: ext - supersorts of this sort, which have to be eitherconcrete sorts or plain generic sorts (i.e. |
ext | SetOfSort ext(Code) | | direct supersorts
|
oneOf | SetOfSort oneOf(Code) | | list of sorts this generic sort may be instantiated with;
EMPTY_SORT_SORT means that every sort may be used
|
GenericSort | public GenericSort(Name name)(Code) | | creates a generic sort (with a new equality symbol for this
sort)
|
GenericSort | public GenericSort(Name name, SetOfSort ext, SetOfSort oneOf) throws GenericSupersortException(Code) | | creates a generic sort
Parameters: ext - supersorts of this sort, which have to be eitherconcrete sorts or plain generic sorts (i.e. not collectionsorts of generic sorts) |
checkNonGenericSupersorts | protected boolean checkNonGenericSupersorts(Sort p_s)(Code) | | true iff "p_s" is subsort of every non-genericsupersort of this sort |
extendsSorts | public SetOfSort extendsSorts()(Code) | | direct supersorts |
getOneOf | public SetOfSort getOneOf()(Code) | | possible instantiations or "EMPTY_SORT_SET" |
isPossibleInstantiation | public boolean isPossibleInstantiation(Sort p_s)(Code) | | true if "p_s" is a possible instantiation of thissort. This method does not check the instantiations of othergeneric sorts, i.e. the return value true is possible even if"p_s" is not a valid instantiation.Use "GenericSortInstantiations" instead |
|
|