public class ExecutionMethodReturn extends AbstractExecutionMethodReturn<SourceElement> implements IExecutionMethodReturn
IExecutionMethodReturn
.Modifier and Type | Field and Description |
---|---|
private String |
nameIncludingReturnValue
The node name including the return value.
|
private IExecutionMethodReturnValue[] |
returnValues
The possible return values.
|
private String |
signatureIncludingReturnValue
The node name with signature including the return value.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected String |
computeCalledMethodName()
Computes the name of the called method.
|
protected String |
computeCalledMethodSignature()
Computes the signature of the called method.
|
static String |
createMethodReturnName(Object returnValue,
String methodName)
Creates the human readable name which is shown in
IExecutionMethodReturn instances. |
protected Node |
findMethodReturnNode(Node node)
Searches from the given
Node the parent which applies
the rule "methodCallReturn" in the same modality. |
String |
getElementType()
Returns a human readable element type name.
|
String |
getNameIncludingReturnValue()
Returns the human readable node name including the return value (
IExecutionMethodReturn.getReturnValues() ). |
IExecutionMethodReturnValue[] |
getReturnValues()
Returns the possible return values.
|
String |
getSignatureIncludingReturnValue()
Returns the human readable signature including the return value (
IExecutionMethodReturn.getReturnValues() ). |
boolean |
isReturnValuesComputed()
Checks if the values of
IExecutionMethodReturn.getReturnValues() are already computed. |
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() 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 |
lazyComputeNameIncludingReturnValue()
Computes the name including the return value lazily when
getNameIncludingReturnValue() is called the first time. |
protected IExecutionMethodReturnValue[] |
lazyComputeReturnValues()
Computes the return value lazily when
#getReturnValue() is called the first time. |
protected String |
lazyComputeSignature()
Computes the signature lazily when
AbstractExecutionMethodReturn.getSignature() is called the first time. |
protected String |
lazyComputeSigntureIncludingReturnValue()
Computes the signature including the return value lazily when
getNameIncludingReturnValue() is called the first time. |
getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature, lazyComputeCallStateVariables, lazyComputeMethodReturnCondition
addChild, addCompletedBlock, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, setCallStack, setParent
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private String signatureIncludingReturnValue
private String nameIncludingReturnValue
private IExecutionMethodReturnValue[] returnValues
public ExecutionMethodReturn(ITreeSettings settings, Node proofNode, ExecutionMethodCall methodCall)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.methodCall
- The IExecutionMethodCall
which is now returned.protected String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
protected String computeCalledMethodName()
protected String lazyComputeSignature() throws ProofInputException
AbstractExecutionMethodReturn.getSignature()
is called the first time.lazyComputeSignature
in class AbstractExecutionMethodReturn<SourceElement>
ProofInputException
protected String computeCalledMethodSignature() throws ProofInputException
ProofInputException
public String getNameIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getNameIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.protected String lazyComputeNameIncludingReturnValue() throws ProofInputException
getNameIncludingReturnValue()
is called the first time.Occurred
- Exception.ProofInputException
public String getSignatureIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getSignatureIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.protected String lazyComputeSigntureIncludingReturnValue() throws ProofInputException
getNameIncludingReturnValue()
is called the first time.Occurred
- Exception.ProofInputException
public IExecutionMethodReturnValue[] getReturnValues() throws ProofInputException
getReturnValues
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.public boolean isReturnValuesComputed()
IExecutionMethodReturn.getReturnValues()
are already computed.isReturnValuesComputed
in interface IExecutionMethodReturn
true
value of IExecutionMethodReturn.getReturnValues()
are already computed, false
values of IExecutionMethodReturn.getReturnValues()
needs to be computed.protected IExecutionMethodReturnValue[] lazyComputeReturnValues() throws ProofInputException
#getReturnValue()
is called the first time.ProofInputException
- Occurred Exception.protected Node findMethodReturnNode(Node node)
Node
the parent which applies
the rule "methodCallReturn" in the same modality.public static String createMethodReturnName(Object returnValue, String methodName)
IExecutionMethodReturn
instances.returnValue
- The return value.methodName
- The name of the method that is completely executed.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.public String getElementType()
getElementType
in interface IExecutionElement