public class ExecutionMethodReturnValue extends AbstractExecutionElement implements IExecutionMethodReturnValue
IExecutionMethodReturnValue
.Modifier and Type | Field and Description |
---|---|
private Term |
condition
The optional condition.
|
private java.lang.String |
conditionString
The optional condition as human readable
String . |
private PosInOccurrence |
modalityPIO
The
PosInOccurrence of the modality of interest. |
private Term |
returnValue
The return value.
|
private java.lang.String |
returnValueString
The return value as human readable
String . |
Constructor and Description |
---|
ExecutionMethodReturnValue(ITreeSettings settings,
Node proofNode,
PosInOccurrence modalityPIO,
Term returnValue,
Term condition)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Term |
getCondition()
Returns the optional condition under which the return value is valid.
|
java.lang.String |
getConditionString()
Returns the optional condition under which the return value is valid
as human readable
String . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
PosInOccurrence |
getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
Term |
getReturnValue()
Returns the return value.
|
java.lang.String |
getReturnValueString()
Returns the return value as human readable
String . |
boolean |
hasCondition()
Checks if a condition is available via
IExecutionMethodReturnValue.getCondition()
under which this return value is returned. |
protected java.lang.String |
lazyComputeConditionString()
Computes the human readable return value of this node lazily when
getConditionString()
is called the first time. |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
lazyComputeReturnValueString()
Computes the human readable return value of this node lazily when
getReturnValueString()
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
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final Term returnValue
private final PosInOccurrence modalityPIO
PosInOccurrence
of the modality of interest.private java.lang.String returnValueString
String
.private final Term condition
private java.lang.String conditionString
String
.public ExecutionMethodReturnValue(ITreeSettings settings, Node proofNode, PosInOccurrence modalityPIO, Term returnValue, Term condition)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.returnValue
- The return value.condition
- The optional condition or null
if no condition is available.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
public Term getReturnValue() throws ProofInputException
getReturnValue
in interface IExecutionMethodReturnValue
ProofInputException
- Occurred Exception.public java.lang.String getReturnValueString() throws ProofInputException
String
.getReturnValueString
in interface IExecutionMethodReturnValue
String
.ProofInputException
- Occurred Exception.protected java.lang.String lazyComputeReturnValueString() throws ProofInputException
getReturnValueString()
is called the first time.ProofInputException
public boolean hasCondition() throws ProofInputException
IExecutionMethodReturnValue.getCondition()
under which this return value is returned.hasCondition
in interface IExecutionMethodReturnValue
true
condition is available, false
condition is not available.ProofInputException
public Term getCondition() throws ProofInputException
getCondition
in interface IExecutionMethodReturnValue
ProofInputException
- Occurred Exception.public java.lang.String getConditionString() throws ProofInputException
String
.getConditionString
in interface IExecutionMethodReturnValue
String
.ProofInputException
- Occurred Exception.protected java.lang.String lazyComputeConditionString() throws ProofInputException
getConditionString()
is called the first time.ProofInputException
public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.