public class ExecutionTermination extends AbstractExecutionNode<SourceElement> implements IExecutionTermination
IExecutionTermination
.IExecutionTermination.TerminationKind
Modifier and Type | Field and Description |
---|---|
private Sort |
exceptionSort
The
Sort of the uncaught exception. |
private IProgramVariable |
exceptionVariable
Contains the exception variable which is used to check if the executed program in proof terminates normally.
|
private IExecutionTermination.TerminationKind |
terminationKind
The
TerminationKind . |
LOOP_BODY_TERMINATION_NODE_NAME, NORMAL_TERMINATION_NODE_NAME
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionTermination(ITreeSettings settings,
Node proofNode,
IProgramVariable exceptionVariable,
IExecutionTermination.TerminationKind terminationKind)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
Sort |
getExceptionSort()
Returns the
Sort of the caught exception. |
IProgramVariable |
getExceptionVariable()
Returns the
IProgramVariable which is used in the Sequent
of Proof.root() to check if a normal or exceptional termination
occurred. |
IExecutionTermination.TerminationKind |
getTerminationKind()
Returns the
IExecutionTermination.TerminationKind . |
protected boolean |
isBlockContractTermination()
Checks if a block contract terminates.
|
boolean |
isBranchVerified()
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
protected boolean |
isExceptionalTermination()
Checks if is an exceptional termination.
|
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. |
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 final IProgramVariable exceptionVariable
private IExecutionTermination.TerminationKind terminationKind
TerminationKind
.public ExecutionTermination(ITreeSettings settings, Node proofNode, IProgramVariable exceptionVariable, IExecutionTermination.TerminationKind terminationKind)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.exceptionVariable
- Contains the exception variable which is used to check if the executed program in proof terminates normally.terminationKind
- The TerminationKind
or null
to compute it when it is requested the first time (normal or exceptional termination only).protected java.lang.String lazyComputeName()
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.public IProgramVariable getExceptionVariable()
IProgramVariable
which is used in the Sequent
of Proof.root()
to check if a normal or exceptional termination
occurred.getExceptionVariable
in interface IExecutionTermination
IProgramVariable
which is used to caught global exceptions.public IExecutionTermination.TerminationKind getTerminationKind()
IExecutionTermination.TerminationKind
.getTerminationKind
in interface IExecutionTermination
IExecutionTermination.TerminationKind
.protected boolean isBlockContractTermination()
true
A block contract terminates, false
normal execution terminates.protected boolean isExceptionalTermination()
true
exceptional termination, false
normal termination.public Sort getExceptionSort()
Sort
of the caught exception.getExceptionSort
in interface IExecutionTermination
Sort
of the caught exception.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public boolean isBranchVerified()
isBranchVerified
in interface IExecutionTermination
true
verified/closed, false
not verified/still open