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

Class ExecutionStart

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.ExecutionStart

All Implemented Interfaces:

IExecutionElement, IExecutionNode<SourceElement>, IExecutionStart

public class ExecutionStart
extends AbstractExecutionNode<SourceElement>
implements IExecutionStart

The default implementation of IExecutionStart.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<IExecutionTermination>	terminations The up to know discovered IExecutionTerminations.

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

DEFAULT_START_NODE_NAME

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
ExecutionStart(ITreeSettings settings, Node proofNode) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addTermination(IExecutionTermination termination) Registers the given IExecutionTermination.
SourceElement	getActiveStatement() Returns the active statement which is executed in the code.
java.lang.String	getElementType() Returns a human readable element type name.
ImmutableList<IExecutionTermination>	getTerminations() Returns the up to now discovered IExecutionTerminations.
protected IExecutionConstraint[]	lazyComputeConstraints() Computes the constraints lazily when AbstractExecutionNode.getConstraints() is called the first time.
protected PosInOccurrence	lazyComputeModalityPIO() Computes the PosInOccurrence lazily when AbstractExecutionNode.getModalityPIO() 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.
void	removeTermination(IExecutionTermination termination) Removes the given termination.

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

addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeLayoutExtractor, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent

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

formatTerm, getAppliedRuleApp, 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, 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, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

terminations

private ImmutableList<IExecutionTermination> terminations

The up to know discovered IExecutionTerminations.

Constructor Detail

ExecutionStart

public ExecutionStart(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

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.

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.

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.

getTerminations

public ImmutableList<IExecutionTermination> getTerminations()

Returns the up to now discovered IExecutionTerminations.

Specified by:

getTerminations in interface IExecutionStart

Returns:

The up to now discovered IExecutionTerminations.

addTermination

public void addTermination(IExecutionTermination termination)

Registers the given IExecutionTermination.

Parameters:

termination - The IExecutionTermination to register.

lazyComputeModalityPIO

protected PosInOccurrence lazyComputeModalityPIO()

Computes the PosInOccurrence lazily when AbstractExecutionNode.getModalityPIO() is called the first time.

Overrides:

lazyComputeModalityPIO in class AbstractExecutionNode<SourceElement>

Returns:

The PosInOccurrences of the modality or its updates.

getActiveStatement

public SourceElement getActiveStatement()

Returns the active statement which is executed in the code.

Specified by:

getActiveStatement in interface IExecutionNode<SourceElement>

Overrides:

getActiveStatement in class AbstractExecutionNode<SourceElement>

Returns:

The active statement which is executed in the code.

removeTermination

public void removeTermination(IExecutionTermination termination)

Removes the given termination.

Parameters:

termination - The termination to be deleted.