public abstract class AbstractExecutionVariable extends AbstractExecutionElement implements IExecutionVariable
IExecutionVariable
s.Modifier and Type | Field and Description |
---|---|
private Term |
additionalCondition
An optional additional condition to consider.
|
private Term |
arrayIndex
The index in the parent array.
|
private PosInOccurrence |
modalityPIO
The
PosInOccurrence of the modality of interest. |
private IExecutionValue |
parentValue
The parent
ExecutionValue or null if not available. |
private IProgramVariable |
programVariable
The represented
IProgramVariable which value is shown. |
Constructor and Description |
---|
AbstractExecutionVariable(ITreeSettings settings,
Node proofNode,
IProgramVariable programVariable,
IExecutionValue parentValue,
Term arrayIndex,
Term additionalCondition,
PosInOccurrence modalityPIO)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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. |
boolean |
isArrayIndex()
Checks if the current value is part of a parent array.
|
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
createSelectTerm, getValues
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final IProgramVariable programVariable
IProgramVariable
which value is shown.private final IExecutionValue parentValue
ExecutionValue
or null
if not available.private final Term arrayIndex
private final Term additionalCondition
private final PosInOccurrence modalityPIO
PosInOccurrence
of the modality of interest.public AbstractExecutionVariable(ITreeSettings settings, Node proofNode, IProgramVariable programVariable, IExecutionValue parentValue, Term arrayIndex, Term additionalCondition, PosInOccurrence modalityPIO)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.programVariable
- The represented IProgramVariable
which value is shown.parentValue
- The parent IExecutionValue
or null
if not available.arrayIndex
- The index in the parent array.additionalCondition
- An optional additional condition to consider.modalityPIO
- The PosInOccurrence
of the modality of interest.public Term getAdditionalCondition()
getAdditionalCondition
in interface IExecutionVariable
protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
public IProgramVariable getProgramVariable()
IProgramVariable
which contains the represented value.getProgramVariable
in interface IExecutionVariable
IProgramVariable
which contains the represented value.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 java.lang.String getElementType()
getElementType
in interface IExecutionElement
public IExecutionValue getParentValue()
IExecutionValue
if available.getParentValue
in interface IExecutionVariable
IExecutionValue
if available and null
otherwise.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.