| java.lang.Object
 de.uka.ilkd.key.rule.soundness.SVPartitioning
| SVPartitioning | | public class SVPartitioning (Code) | | Class holding a complete partitioning of all PV- and expression
schema variables in disjoint, non-empty classes (expression SV are
treated like PVSV at this point to make type handling easier). This
is used to cover all possible combinations of variables
instantiated equally. This class is immutable.
|
| Constructor Summary | |
| | SVPartitioning(SVPartition[] p_boundSVs, SVPartition[] p_expressionSVs)
|
| SVPartitioning | | SVPartitioning(SVPartition[] p_boundSVs, SVPartition[] p_expressionSVs)(Code) | | |
| findPartitionings | | public static SVPartitioning[] findPartitionings(ListOfSchemaVariable p_freeSVs, ListOfSchemaVariable p_boundSVs, ListOfSchemaVariable p_expressionSVs)(Code) | | |
| getPartition | | public ListOfSchemaVariable getPartition(int p)(Code) | | partition p as a list |
| getType | | public KeYJavaType getType(int p, SVTypeInfos p_svTypeInfos)(Code) | | the type of an arbitrary element of partitionp for which the type is known; nullif the type is unknown for all elements of partitionp |
| isExpressionSV | | public boolean isExpressionSV(int p)(Code) | | true iff partition p does only exist ofexpression schema variables |
| isNative | | public boolean isNative(int p)(Code) | | |
| size | | public int size()(Code) | | the number of partitions |
|
|