public interface IExecutionLoopInvariant extends IExecutionNode<SourceElement>
A node in the symbolic execution tree which represents a loop invariant application.
The default implementation is ExecutionLoopInvariant
which
is instantiated via a SymbolicExecutionTreeBuilder
instance.
SymbolicExecutionTreeBuilder
,
ExecutionLoopInvariant
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
getLoopInvariant()
Returns the used
LoopSpecification . |
While |
getLoopStatement()
Returns the loop statement which is simulated by its loop invariant.
|
boolean |
isInitiallyValid()
Checks if the loop invariant is initially valid.
|
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
LoopSpecification getLoopInvariant()
LoopSpecification
.LoopSpecification
.While getLoopStatement()
boolean isInitiallyValid()
true
initially valid, false
initially invalid.