public interface Sort extends Named
Modifier and Type | Field and Description |
---|---|
static Sort |
ANY
Any is a supersort of all sorts.
|
static Name |
CAST_NAME
Name of
getCastSymbol(TermServices) . |
static Name |
EXACT_INSTANCE_NAME
|
static Sort |
FORMULA
Formulas are represented as "terms" of this sort.
|
static Name |
INSTANCE_NAME
Name of
getInstanceofSymbol(TermServices) . |
static Sort |
TERMLABEL
Term labels are represented as "terms" of this sort.
|
static Sort |
UPDATE
Updates are represented as "terms" of this sort.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
declarationString() |
ImmutableSet<Sort> |
extendsSorts() |
ImmutableSet<Sort> |
extendsSorts(Services services) |
boolean |
extendsTrans(Sort s) |
SortDependingFunction |
getCastSymbol(TermServices services) |
SortDependingFunction |
getExactInstanceofSymbol(TermServices services) |
SortDependingFunction |
getInstanceofSymbol(TermServices services) |
boolean |
isAbstract() |
static final Sort FORMULA
static final Sort UPDATE
static final Sort TERMLABEL
static final Sort ANY
static final Name CAST_NAME
getCastSymbol(TermServices)
.static final Name INSTANCE_NAME
getInstanceofSymbol(TermServices)
.static final Name EXACT_INSTANCE_NAME
ImmutableSet<Sort> extendsSorts()
NullSort
.ImmutableSet<Sort> extendsSorts(Services services)
services
- services.boolean extendsTrans(Sort s)
s
- some sort.boolean isAbstract()
SortDependingFunction getCastSymbol(TermServices services)
services
- services.SortDependingFunction getInstanceofSymbol(TermServices services)
services
- services.instanceof
symbol of this sort.SortDependingFunction getExactInstanceofSymbol(TermServices services)
services
- services.exactinstanceof
symbol of this sort.java.lang.String declarationString()
Copyright © 2003-2019 The KeY-Project.