public class ExecutionMethodReturnValue extends AbstractExecutionElement implements IExecutionMethodReturnValue
IExecutionMethodReturnValue
.Modifier and Type | Field and Description |
---|---|
private Term |
condition
The optional condition.
|
private 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 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.
|
String |
getConditionString()
Returns the optional condition under which the return value is valid
as human readable
String . |
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.
|
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 String |
lazyComputeConditionString()
Computes the human readable return value of this node lazily when
getConditionString()
is called the first time. |
protected String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected 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 final Term condition
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 String getElementType()
getElementType
in interface IExecutionElement
protected 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 String getReturnValueString() throws ProofInputException
String
.getReturnValueString
in interface IExecutionMethodReturnValue
String
.ProofInputException
- Occurred Exception.protected 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 String getConditionString() throws ProofInputException
String
.getConditionString
in interface IExecutionMethodReturnValue
String
.ProofInputException
- Occurred Exception.protected 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.