public static class ExecutionVariableExtractor.ExtractedExecutionVariable extends AbstractExecutionVariable
IExecutionVariable
instantiated by the ExecutionVariableExtractor
.Constructor and Description |
---|
ExtractedExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term additionalCondition,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Term |
createSelectTerm()
Creates recursive a term which can be used to determine the value
of
IExecutionVariable.getProgramVariable() . |
Term |
getArrayEndIndex()
Returns the array end index.
|
java.lang.String |
getArrayEndIndexString()
Returns the human readable array end index.
|
Term |
getArrayStartIndex()
Returns the array start index.
|
java.lang.String |
getArrayStartIndexString()
Returns the human readable array start index.
|
IExecutionValue[] |
getValues()
Returns the possible values of this
IExecutionVariable . |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getParentValue, getProgramVariable, isArrayIndex
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
public ExtractedExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term arrayIndex, Term arrayStartIndex, Term arrayEndIndex, Term additionalCondition, ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
parentNode
- The IExecutionNode
providing relevant information.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.modalityPIO
- The PosInOccurrence
of the modality of interest.programVariable
- The represented IProgramVariable
which value is shown.arrayIndex
- The index in the parent array.additionalCondition
- An optional additional condition to consider.parentValue
- The parent IExecutionValue
or null
if not available.public IExecutionValue[] getValues() throws ProofInputException
IExecutionVariable
.IExecutionVariable
.ProofInputException
public Term createSelectTerm()
IExecutionVariable.getProgramVariable()
.public Term getArrayStartIndex()
public java.lang.String getArrayStartIndexString()
public Term getArrayEndIndex()
public java.lang.String getArrayEndIndexString()
protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionVariable
IExecutionNode
.ProofInputException
Copyright © 2003-2019 The KeY-Project.