public abstract class AbstractExecutionMethodReturn<S extends SourceElement> extends AbstractExecutionNode<S> implements IExecutionBaseMethodReturn<S>
IExecutionBaseMethodReturn
.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
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
Copyright © 2003-2019 The KeY-Project.