public static class ExecutionNodeReader.KeYlessOperationContract extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionOperationContract
IExecutionOperationContract
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
formatedContractParams
The formated contract parameters.
|
private java.lang.String |
formatedExceptionTerm
The formated exception term.
|
private java.lang.String |
formatedResultTerm
The formated result term.
|
private java.lang.String |
formatedSelfTerm
The formated self term.
|
private boolean |
hasNotNullCheck
Has not null check?
|
private boolean |
notNullCheckComplied
Is not null check complied?
|
private boolean |
preconditionComplied
Is precondition complied?
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessOperationContract(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean preconditionComplied,
boolean hasNotNullCheck,
boolean notNullCheckComplied,
java.lang.String formatedResultTerm,
java.lang.String formatedExceptionTerm,
java.lang.String formatedSelfTerm,
java.lang.String formatedContractParams)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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.
|
addCallStackEntry, addChild, addCompletedBlock, addConstraint, addIncomingLink, addOutgoingLink, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, 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 final boolean preconditionComplied
private final boolean hasNotNullCheck
private final boolean notNullCheckComplied
private final java.lang.String formatedResultTerm
private final java.lang.String formatedExceptionTerm
private final java.lang.String formatedSelfTerm
private final java.lang.String formatedContractParams
public KeYlessOperationContract(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean preconditionComplied, boolean hasNotNullCheck, boolean notNullCheckComplied, java.lang.String formatedResultTerm, java.lang.String formatedExceptionTerm, java.lang.String formatedSelfTerm, java.lang.String formatedContractParams)
parent
- The parent IExecutionNode
.name
- The name of this node.pathConditionChanged
- Is the path condition changed compared to parent?formatedPathCondition
- The formated path condition.preconditionComplied
- Is precondition complied?hasNotNullCheck
- Has not null check?notNullCheckComplied
- Is not null check complied?formatedResultTerm
- The formated result term.formatedExceptionTerm
- The formated exception term.formatedSelfTerm
- The formated self term.formatedContractParams
- The formated contract parameters.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
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 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.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 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 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 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.