public class ExecutionLoopInvariant extends AbstractExecutionNode<SourceElement> implements IExecutionLoopInvariant
IExecutionLoopInvariant
.INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionLoopInvariant(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
LoopInvariantBuiltInRuleApp |
getAppliedRuleApp()
Returns the applied
RuleApp . |
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.
|
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, 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
getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
public ExecutionLoopInvariant(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.public LoopInvariantBuiltInRuleApp getAppliedRuleApp()
RuleApp
.getAppliedRuleApp
in interface IExecutionElement
getAppliedRuleApp
in class AbstractExecutionElement
RuleApp
.protected java.lang.String lazyComputeName()
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.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 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.