public final class ParameterlessTermLabel extends java.lang.Object implements TermLabel
ParameterlessTermLabel
can be used to define labels without parameters.
You can use a SingletonLabelFactory
to create a factory for an
instance of this class.SingletonLabelFactory
Modifier and Type | Field and Description |
---|---|
static TermLabel |
ANON_HEAP_LABEL
Label attached to anonymisation heap function symbols as for instance
introduce in UseOperationContractRule or WhileInvariantRule.
|
static Name |
ANON_HEAP_LABEL_NAME
Name of
ANON_HEAP_LABEL . |
static TermLabel |
IMPLICIT_SPECIFICATION_LABEL
Label attached to a term which is specified implicitly (by the JML specification).
|
static Name |
IMPLICIT_SPECIFICATION_LABEL_NAME
Name of
IMPLICIT_SPECIFICATION_LABEL . |
static TermLabel |
LOOP_SCOPE_INDEX_LABEL
Label attached to loop scope index variables in
LoopScopeInvariantRule . |
static Name |
LOOP_SCOPE_INDEX_LABEL_NAME
Name of
LOOP_SCOPE_INDEX_LABEL . |
private Name |
name
The unique name of this label.
|
static TermLabel |
POST_CONDITION_LABEL |
static Name |
POST_CONDITION_LABEL_NAME
Label attached to the post condition.
|
static TermLabel |
SELECT_SKOLEM_LABEL
Label attached to skolem constants introduced by the rule pullOutSelect.
|
static Name |
SELECT_SKOLEM_LABEL_NAME
Name of
SELECT_SKOLEM_LABEL . |
static TermLabel |
SELF_COMPOSITION_LABEL
Label attached to the post condition.
|
static Name |
SELF_COMPOSITION_LABEL_NAME
Name of
SELF_COMPOSITION_LABEL . |
static TermLabel |
SHORTCUT_EVALUATION_LABEL
Label attached to a term with the logical operator '||' or
'&&' to distinguish from '|' or '&'
respectively.
|
static Name |
SHORTCUT_EVALUATION_LABEL_NAME
Name of
SHORTCUT_EVALUATION_LABEL . |
static TermLabel |
UNDEFINED_VALUE_LABEL
Label attached to a term which denotes an undefined value.
|
static Name |
UNDEFINED_VALUE_LABEL_NAME
Name of
UNDEFINED_VALUE_LABEL . |
Constructor and Description |
---|
ParameterlessTermLabel(Name name)
Instantiates a new simple term label.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object obj)
This object is equal to another
ParameterlessTermLabel iff they
bear the same name. |
java.lang.Object |
getChild(int i)
Retrieves the i-th parameter object of this term label.
|
int |
getChildCount()
Gets the number of parameters of this term label.
|
int |
hashCode() |
Name |
name()
returns the name of this element
|
java.lang.String |
toString() |
public static final Name ANON_HEAP_LABEL_NAME
ANON_HEAP_LABEL
.public static final TermLabel ANON_HEAP_LABEL
public static final Name SELECT_SKOLEM_LABEL_NAME
SELECT_SKOLEM_LABEL
.public static final TermLabel SELECT_SKOLEM_LABEL
public static final Name IMPLICIT_SPECIFICATION_LABEL_NAME
IMPLICIT_SPECIFICATION_LABEL
.public static final TermLabel IMPLICIT_SPECIFICATION_LABEL
public static final Name SHORTCUT_EVALUATION_LABEL_NAME
SHORTCUT_EVALUATION_LABEL
.public static final TermLabel SHORTCUT_EVALUATION_LABEL
public static final Name UNDEFINED_VALUE_LABEL_NAME
UNDEFINED_VALUE_LABEL
.public static final TermLabel UNDEFINED_VALUE_LABEL
IfExThenElse
operator,
when it is used for the translation of JML's \min and \max operator. It is necessary
to evaluate this constant expression to be not well-defined.public static final Name SELF_COMPOSITION_LABEL_NAME
SELF_COMPOSITION_LABEL
.public static final TermLabel SELF_COMPOSITION_LABEL
public static final Name POST_CONDITION_LABEL_NAME
public static final TermLabel POST_CONDITION_LABEL
public static final Name LOOP_SCOPE_INDEX_LABEL_NAME
LOOP_SCOPE_INDEX_LABEL
.public static final TermLabel LOOP_SCOPE_INDEX_LABEL
LoopScopeInvariantRule
.private final Name name
public ParameterlessTermLabel(Name name)
name
- the name, not null
The fixed associated instantiator, may be null
.public java.lang.Object getChild(int i)
A term label may have structure, i.e. can be parameterized.
Simple term labels have no parameters. This always throws an
IndexOutOfBoundsException
.
public int getChildCount()
Simple term labels have no parameters. This always returns 0.
getChildCount
in interface TermLabel
public java.lang.String toString()
toString
in class java.lang.Object
public boolean equals(java.lang.Object obj)
This object is equal to another ParameterlessTermLabel
iff they
bear the same name.
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object