public final class ArraySort extends AbstractSort
More precisely, there can be one array sort for every pair (element sort, element type); i.e., there can be several array sorts for the same element sort, distinguished by their element *type*. This is used for the integer types of Java: these are all mapped to the sort "int" (i.e., the mathematical integers), but we have different array sorts int[], byte[], char[], short[] and long[], all storing mathematical integers.
ANY, CAST_NAME, EXACT_INSTANCE_NAME, FORMULA, INSTANCE_NAME, TERMLABEL, UPDATE
Modifier and Type | Method and Description |
---|---|
Sort |
elementSort()
returns the element sort of the array
|
static ArraySort |
getArraySort(Sort elemSort,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort) |
static ArraySort |
getArraySort(Sort elemSort,
Type elemType,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort)
Returns the ArraySort to the given element sort and element type.
|
static Sort |
getArraySortForDim(Sort elemSort,
Type elemType,
int n,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort)
returns elemSort([])^n.
|
declarationString, extendsSorts, extendsSorts, extendsTrans, getCastSymbol, getExactInstanceofSymbol, getInstanceofSymbol, isAbstract, name, toString
public static ArraySort getArraySort(Sort elemSort, Type elemType, Sort objectSort, Sort cloneableSort, Sort serializableSort)
public static ArraySort getArraySort(Sort elemSort, Sort objectSort, Sort cloneableSort, Sort serializableSort)
public static Sort getArraySortForDim(Sort elemSort, Type elemType, int n, Sort objectSort, Sort cloneableSort, Sort serializableSort)
public Sort elementSort()
Copyright © 2003-2019 The KeY-Project.