private class ExecutionVariableExtractor.StateExecutionVariable extends AbstractExecutionVariable
IExecutionVariable
instantiated by the ExecutionVariableExtractor
.Modifier and Type | Field and Description |
---|---|
private IExecutionValue[] |
values
The contained
IExecutionValue s. |
Constructor and Description |
---|
StateExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term additionalCondition)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Term |
createSelectTerm()
Creates recursive a term which can be used to determine the value
of
IExecutionVariable.getProgramVariable() . |
IExecutionValue[] |
getValues()
Returns the possible values of this
IExecutionVariable . |
getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getParentValue, getProgramVariable, isArrayIndex, lazyComputeName
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
private IExecutionValue[] values
IExecutionValue
s.public StateExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term arrayIndex, Term additionalCondition)
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.public IExecutionValue[] getValues() throws ProofInputException
IExecutionVariable
.IExecutionVariable
.ProofInputException
public Term createSelectTerm()
IExecutionVariable.getProgramVariable()
.