public final class ParameterlessTermLabel extends 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 . |
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(Object obj) |
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
|
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
private final Name name
public ParameterlessTermLabel(Name name)
name
- the name, not null
instantiator
- the fixed associated instantiator, may be null
.public 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 boolean equals(Object obj)
This object is equal to another ParameterlessTermLabel
iff they
bear the same name.