public static class ExecutionNodeReader.KeYlessLoopInvariant extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionLoopInvariant
IExecutionLoopInvariant
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private boolean |
initiallyValid
Initially valid?
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessLoopInvariant(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean initiallyValid)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
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.
|
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
public KeYlessLoopInvariant(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean initiallyValid)
parent
- The parent IExecutionNode
.name
- The name of this node.pathConditionChanged
- Is the path condition changed compared to parent?formatedPathCondition
- The formated path condition.initiallyValid
- Initially valid?public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public LoopSpecification getLoopInvariant()
LoopSpecification
.getLoopInvariant
in interface IExecutionLoopInvariant
LoopSpecification
.public While getLoopStatement()
getLoopStatement
in interface IExecutionLoopInvariant
public boolean isInitiallyValid()
isInitiallyValid
in interface IExecutionLoopInvariant
true
initially valid, false
initially invalid.