static enum BasicSnippetData.Key extends java.lang.Enum<BasicSnippetData.Key>
Enum Constant and Description |
---|
BLOCK_SELF
Self term of the transformed block contract
|
BLOCK_VARS
Variables originally used during parsing.
|
DEPENDENS |
EXECUTION_CONTEXT |
FOR_CLASS
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
INF_FLOW_SPECS |
LABELS |
LOOP_INVARIANT |
LOOP_INVARIANT_TERM |
MEASURED_BY |
MODALITY |
MODIFIES |
POSTCONDITION |
PRECONDITION |
TARGET_BLOCK
Returns the contracted block.
|
TARGET_METHOD
Returns the contracted function symbol.
|
Modifier and Type | Field and Description |
---|---|
private java.lang.Class<?> |
type |
Modifier and Type | Method and Description |
---|---|
java.lang.Class<?> |
getType() |
static BasicSnippetData.Key |
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static BasicSnippetData.Key[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
public static final BasicSnippetData.Key FOR_CLASS
public static final BasicSnippetData.Key TARGET_METHOD
public static final BasicSnippetData.Key TARGET_BLOCK
public static final BasicSnippetData.Key PRECONDITION
public static final BasicSnippetData.Key POSTCONDITION
public static final BasicSnippetData.Key LOOP_INVARIANT
public static final BasicSnippetData.Key LOOP_INVARIANT_TERM
public static final BasicSnippetData.Key MODIFIES
public static final BasicSnippetData.Key DEPENDENS
public static final BasicSnippetData.Key MEASURED_BY
public static final BasicSnippetData.Key MODALITY
public static final BasicSnippetData.Key INF_FLOW_SPECS
public static final BasicSnippetData.Key BLOCK_SELF
public static final BasicSnippetData.Key BLOCK_VARS
public static final BasicSnippetData.Key LABELS
public static final BasicSnippetData.Key EXECUTION_CONTEXT
public static BasicSnippetData.Key[] values()
for (BasicSnippetData.Key c : BasicSnippetData.Key.values()) System.out.println(c);
public static BasicSnippetData.Key valueOf(java.lang.String name)
name
- the name of the enum constant to be returned.java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is nullpublic java.lang.Class<?> getType()