de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionLoopInvariant

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionLoopInvariant, ExecutionNodeReader.KeYlessLoopInvariant

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.

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionLoopInvariant

Field Summary

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Method Summary

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.

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Method Detail

getLoopInvariant

LoopSpecification getLoopInvariant()

Returns the used LoopSpecification.

Returns:

The used LoopSpecification.

getLoopStatement

While getLoopStatement()

Returns the loop statement which is simulated by its loop invariant.

Returns:

The loop statement which is simulated by its loop invariant.

isInitiallyValid

boolean isInitiallyValid()

Checks if the loop invariant is initially valid.

Returns:

true initially valid, false initially invalid.