public static class ExecutionNodeReader.KeYlessMethodReturnValue extends ExecutionNodeReader.AbstractKeYlessExecutionElement implements IExecutionMethodReturnValue
IExecutionMethodReturn
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
conditionString
The optional human readable condition.
|
private boolean |
hasCondition
Is a condition available?
|
private java.lang.String |
returnValueString
The human readable return value.
|
Constructor and Description |
---|
KeYlessMethodReturnValue(java.lang.String name,
java.lang.String returnValueString,
boolean hasCondition,
java.lang.String conditionString)
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. |
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final java.lang.String returnValueString
private final boolean hasCondition
private final java.lang.String conditionString
public KeYlessMethodReturnValue(java.lang.String name, java.lang.String returnValueString, boolean hasCondition, java.lang.String conditionString)
name
- The name of this node.returnValueString
- The human readable return value.hasCondition
- Is a condition available?conditionString
- The optional human readable condition.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
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.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.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.