de.uka.ilkd.key.symbolic_execution.model.impl

Class ExecutionLoopInvariant

java.lang.Object

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode<SourceElement>

de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionLoopInvariant

All Implemented Interfaces:

IExecutionElement, IExecutionLoopInvariant, IExecutionNode<SourceElement>

public class ExecutionLoopInvariant
extends AbstractExecutionNode<SourceElement>
implements IExecutionLoopInvariant

The default implementation of IExecutionLoopInvariant.

Author:

Martin Hentschel

Field Summary

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

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
ExecutionLoopInvariant(ITreeSettings settings, Node proofNode) Constructor.

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode

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

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

formatTerm, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

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

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

Constructor Detail

ExecutionLoopInvariant

public ExecutionLoopInvariant(ITreeSettings settings,
                              Node proofNode)

Constructor.

Parameters:

settings - The ITreeSettings to use.

proofNode - The Node of KeY's proof tree which is represented by this IExecutionNode.

Method Detail

getAppliedRuleApp

public LoopInvariantBuiltInRuleApp getAppliedRuleApp()

Returns the applied RuleApp.

Specified by:

getAppliedRuleApp in interface IExecutionElement

Overrides:

getAppliedRuleApp in class AbstractExecutionElement

Returns:

The applied RuleApp.

lazyComputeName

protected java.lang.String lazyComputeName()

Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.

Specified by:

lazyComputeName in class AbstractExecutionElement

Returns:

The human readable name of this IExecutionNode.

getElementType

public java.lang.String getElementType()

Returns a human readable element type name.

Specified by:

getElementType in interface IExecutionElement

Returns:

The human readable element type.

lazyComputeConstraints

protected IExecutionConstraint[] lazyComputeConstraints()

Computes the constraints lazily when AbstractExecutionNode.getConstraints() is called the first time.

Specified by:

lazyComputeConstraints in class AbstractExecutionNode<SourceElement>

Returns:

The IExecutionConstraints of the current state.

getLoopInvariant

public LoopSpecification getLoopInvariant()

Returns the used LoopSpecification.

Specified by:

getLoopInvariant in interface IExecutionLoopInvariant

Returns:

The used LoopSpecification.

getLoopStatement

public While getLoopStatement()

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

Specified by:

getLoopStatement in interface IExecutionLoopInvariant

Returns:

The loop statement which is simulated by its loop invariant.

isInitiallyValid

public boolean isInitiallyValid()

Checks if the loop invariant is initially valid.

Specified by:

isInitiallyValid in interface IExecutionLoopInvariant

Returns:

true initially valid, false initially invalid.