public static class ExecutionNodeReader.KeYlessVariable extends ExecutionNodeReader.AbstractKeYlessExecutionElement implements IExecutionVariable
IExecutionVariable
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
arrayIndexString
The array index.
|
private boolean |
isArrayIndex
The is array flag.
|
private IExecutionValue |
parentValue
The parent
IExecutionValue if available. |
private java.util.List<IExecutionValue> |
values
The contained values.
|
Constructor and Description |
---|
KeYlessVariable(IExecutionValue parentValue,
boolean isArrayIndex,
java.lang.String arrayIndexString,
java.lang.String name)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addValue(IExecutionValue variable)
Adds the given child
IExecutionValue . |
Term |
createSelectTerm()
Creates recursive a term which can be used to determine the value
of
IExecutionVariable.getProgramVariable() . |
Term |
getAdditionalCondition()
Returns the optional additional condition considered during value computation.
|
Term |
getArrayIndex()
Returns the index in the parent array if an array cell value is represented.
|
java.lang.String |
getArrayIndexString()
Returns the human readable index in the parent array if an array cell value is represented.
|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
PosInOccurrence |
getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
IExecutionValue |
getParentValue()
Returns the parent
IExecutionValue if available. |
IProgramVariable |
getProgramVariable()
Returns the
IProgramVariable which contains the represented value. |
IExecutionValue[] |
getValues()
Returns the possible values of this
IExecutionVariable . |
boolean |
isArrayIndex()
Checks if the current value is part of a parent array.
|
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final IExecutionValue parentValue
IExecutionValue
if available.private final boolean isArrayIndex
private final java.lang.String arrayIndexString
private final java.util.List<IExecutionValue> values
public KeYlessVariable(IExecutionValue parentValue, boolean isArrayIndex, java.lang.String arrayIndexString, java.lang.String name)
parentVariable
- The parent IExecutionValue
if available.isArrayIndex
- The is array flag.arrayIndexString
- The array index.name
- The name.public void addValue(IExecutionValue variable)
IExecutionValue
.variable
- The child IExecutionValue
to add.public IExecutionValue getParentValue()
IExecutionValue
if available.getParentValue
in interface IExecutionVariable
IExecutionValue
if available and null
otherwise.public IExecutionValue[] getValues()
IExecutionVariable
.getValues
in interface IExecutionVariable
IExecutionVariable
.public Term getArrayIndex()
getArrayIndex
in interface IExecutionVariable
null
if no array cell value is represented.public java.lang.String getArrayIndexString()
getArrayIndexString
in interface IExecutionVariable
null
if no array cell value is represented.public boolean isArrayIndex()
isArrayIndex
in interface IExecutionVariable
true
is array cell value, false
is a "normal" value.public IProgramVariable getProgramVariable()
IProgramVariable
which contains the represented value.getProgramVariable
in interface IExecutionVariable
IProgramVariable
which contains the represented value.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public Term getAdditionalCondition()
getAdditionalCondition
in interface IExecutionVariable
public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.public Term createSelectTerm()
IExecutionVariable.getProgramVariable()
.createSelectTerm
in interface IExecutionVariable