public class ExecutionOperationContract extends AbstractExecutionNode<SourceElement> implements IExecutionOperationContract
IExecutionOperationContract
.Modifier and Type | Field and Description |
---|---|
private ImmutableList<Term> |
contractParams
The current contract parameters.
|
private Term |
exceptionTerm
|
private Term |
resultTerm
|
private Term |
selfTerm
The self
Term or null if not available. |
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionOperationContract(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected static LocationVariable |
extractResultVariableFromPostBranch(Node node,
Services services)
Extracts the result variable from the given post branch.
|
Contract |
getContract()
Returns the applied
Contract . |
ImmutableList<Term> |
getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
IProgramMethod |
getContractProgramMethod()
Returns the
IProgramMethod of the applied Contract . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
Term |
getExceptionTerm()
|
java.lang.String |
getFormatedContractParams()
Returns the human readable parameters of the called method for which a
Contract is applied. |
java.lang.String |
getFormatedExceptionTerm()
|
java.lang.String |
getFormatedResultTerm()
|
java.lang.String |
getFormatedSelfTerm()
|
Term |
getResultTerm()
|
Term |
getSelfTerm()
|
boolean |
hasNotNullCheck()
Checks if a not null check is available (instance method) or not (static method or constructor).
|
boolean |
isNotNullCheckComplied()
Checks if the not null check is complied.
|
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected Term |
searchConstructorSelfDefinition(Term term,
KeYJavaType staticType,
Services services)
Tries to find the self
Term of the given KeYJavaType . |
protected Term |
searchResultTerm(FunctionalOperationContract contract,
UseOperationContractRule.Instantiation inst,
Services services)
Searches the result
Term . |
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, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, 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
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private Term exceptionTerm
private Term resultTerm
private ImmutableList<Term> contractParams
public ExecutionOperationContract(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
protected Term searchConstructorSelfDefinition(Term term, KeYJavaType staticType, Services services)
Term
of the given KeYJavaType
.term
- The Term
to start search in.staticType
- The expected KeYJavaType
.services
- The Services
to use.Term
or null
if not available.public Term getResultTerm() throws ProofInputException
getResultTerm
in interface IExecutionOperationContract
Term
in which the result of the applied Contract
is stored.ProofInputException
- Occurred Exception.public Term getExceptionTerm() throws ProofInputException
getExceptionTerm
in interface IExecutionOperationContract
Term
in which a by the Contract
thrown Exception
is stored.ProofInputException
- Occurred Exception.public Term getSelfTerm() throws ProofInputException
getSelfTerm
in interface IExecutionOperationContract
Term
or null
if not available.ProofInputException
- Occurred Exception.public ImmutableList<Term> getContractParams() throws ProofInputException
Contract
is applied.getContractParams
in interface IExecutionOperationContract
Contract
is applied.ProofInputException
- Occurred Exception.public java.lang.String getFormatedResultTerm() throws ProofInputException
getFormatedResultTerm
in interface IExecutionOperationContract
Term
in which the result of the applied Contract
is stored.ProofInputException
- Occurred Exception.public java.lang.String getFormatedExceptionTerm() throws ProofInputException
getFormatedExceptionTerm
in interface IExecutionOperationContract
Term
in which a by the Contract
thrown Exception
is stored.ProofInputException
- Occurred Exception.public java.lang.String getFormatedSelfTerm() throws ProofInputException
getFormatedSelfTerm
in interface IExecutionOperationContract
Term
or null
if not available.ProofInputException
- Occurred Exception.public java.lang.String getFormatedContractParams() throws ProofInputException
Contract
is applied.getFormatedContractParams
in interface IExecutionOperationContract
Contract
is applied.ProofInputException
- Occurred Exception.protected Term searchResultTerm(FunctionalOperationContract contract, UseOperationContractRule.Instantiation inst, Services services)
Term
.contract
- The FunctionalOperationContract
.inst
- The UseOperationContractRule.Instantiation
.services
- The Services
.Term
or null
otherwise.protected static LocationVariable extractResultVariableFromPostBranch(Node node, Services services)
node
- The Node
which is the post or exceptional post branch of an applied ContractRuleApp
.services
- The Services
to use.LocationVariable
or null
if not found.public Contract getContract()
Contract
.getContract
in interface IExecutionOperationContract
Contract
.public IProgramMethod getContractProgramMethod()
IProgramMethod
of the applied Contract
.getContractProgramMethod
in interface IExecutionOperationContract
IProgramMethod
of the applied Contract
.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.public boolean isPreconditionComplied()
isPreconditionComplied
in interface IExecutionOperationContract
true
precondition complied, false
precondition not complied.public boolean hasNotNullCheck()
hasNotNullCheck
in interface IExecutionOperationContract
true
not null check available, false
not null check is not available.public boolean isNotNullCheckComplied()
isNotNullCheckComplied
in interface IExecutionOperationContract
true
not null check complied, false
not null check not complied.