public abstract class AbstractExecutionMethodReturn<S extends SourceElement> extends AbstractExecutionNode<S> implements IExecutionBaseMethodReturn<S>
IExecutionBaseMethodReturn
.Modifier and Type | Field and Description |
---|---|
private IExecutionVariable[] |
callStateVariables
The variable value pairs of the state when the method has been called.
|
private java.lang.String |
formatedMethodReturnCondition
The human readable method return condition to reach this node from its calling
IExecutionMethodCall . |
private ExecutionMethodCall |
methodCall
The
IExecutionMethodCall which is now returned. |
private Term |
methodReturnCondition
The method return condition to reach this node from its calling
IExecutionMethodCall . |
private java.lang.String |
signature
The signature.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractExecutionMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
getCallStateVariables()
Returns the variable value pairs of the state when the method has been called.
|
java.lang.String |
getFormatedMethodReturnCondition()
Returns the human readable condition under which this method return is reached from
the calling
IExecutionMethodCall . |
IExecutionMethodCall |
getMethodCall()
A reference to the
IExecutionMethodCall which is now returned. |
Term |
getMethodReturnCondition()
Returns the condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
getSignature()
Returns a human readable signature which describes this element.
|
protected IExecutionVariable[] |
lazyComputeCallStateVariables()
Computes the variables lazily when
getCallStateVariables() is
called the first time. |
protected void |
lazyComputeMethodReturnCondition()
Computes the method return condition lazily when
getMethodReturnCondition()
or getFormatedMethodReturnCondition() is called the first time. |
protected abstract java.lang.String |
lazyComputeSignature()
Computes the signature lazily when
getSignature() is called the first time. |
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeConstraints, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, lazyComputeName, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final ExecutionMethodCall methodCall
IExecutionMethodCall
which is now returned.private java.lang.String signature
private Term methodReturnCondition
IExecutionMethodCall
.private java.lang.String formatedMethodReturnCondition
IExecutionMethodCall
.private IExecutionVariable[] callStateVariables
public AbstractExecutionMethodReturn(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.public IExecutionMethodCall getMethodCall()
IExecutionMethodCall
which is now returned.getMethodCall
in interface IExecutionBaseMethodReturn<S extends SourceElement>
public java.lang.String getSignature() throws ProofInputException
getSignature
in interface IExecutionBaseMethodReturn<S extends SourceElement>
ProofInputException
- Occurred Exception.protected abstract java.lang.String lazyComputeSignature() throws ProofInputException
getSignature()
is called the first time.Occurred
- Exception.ProofInputException
public Term getMethodReturnCondition() throws ProofInputException
IExecutionMethodCall
.getMethodReturnCondition
in interface IExecutionBaseMethodReturn<S extends SourceElement>
IExecutionMethodCall
as Term
.ProofInputException
public java.lang.String getFormatedMethodReturnCondition() throws ProofInputException
IExecutionMethodCall
.getFormatedMethodReturnCondition
in interface IExecutionBaseMethodReturn<S extends SourceElement>
IExecutionMethodCall
.ProofInputException
protected void lazyComputeMethodReturnCondition() throws ProofInputException
getMethodReturnCondition()
or getFormatedMethodReturnCondition()
is called the first time.ProofInputException
- Occurred Exceptionpublic IExecutionVariable[] getCallStateVariables() throws ProofInputException
getCallStateVariables
in interface IExecutionBaseMethodReturn<S extends SourceElement>
ProofInputException
protected IExecutionVariable[] lazyComputeCallStateVariables() throws ProofInputException
getCallStateVariables()
is
called the first time.IExecutionVariable
s of the state when the method has been called.ProofInputException