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

Class ExecutionTermination

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

All Implemented Interfaces:

IExecutionElement, IExecutionNode<SourceElement>, IExecutionTermination

public class ExecutionTermination
extends AbstractExecutionNode<SourceElement>
implements IExecutionTermination

The default implementation of IExecutionTermination.

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination

IExecutionTermination.TerminationKind

Field Summary

Fields

Modifier and Type	Field and Description
private Sort	exceptionSort The Sort of the uncaught exception.
private IProgramVariable	exceptionVariable Contains the exception variable which is used to check if the executed program in proof terminates normally.
private IExecutionTermination.TerminationKind	terminationKind The TerminationKind.

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

LOOP_BODY_TERMINATION_NODE_NAME, NORMAL_TERMINATION_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
ExecutionTermination(ITreeSettings settings, Node proofNode, IProgramVariable exceptionVariable, IExecutionTermination.TerminationKind terminationKind) Constructor.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getElementType() Returns a human readable element type name.
Sort	getExceptionSort() Returns the Sort of the caught exception.
IProgramVariable	getExceptionVariable() Returns the IProgramVariable which is used in the Sequent of Proof.root() to check if a normal or exceptional termination occurred.
IExecutionTermination.TerminationKind	getTerminationKind() Returns the IExecutionTermination.TerminationKind.
protected boolean	isBlockContractTermination() Checks if a block contract terminates.
boolean	isBranchVerified() Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.
protected boolean	isExceptionalTermination() Checks if is an exceptional termination.
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, 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, 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, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

exceptionVariable

private final IProgramVariable exceptionVariable

Contains the exception variable which is used to check if the executed program in proof terminates normally.

exceptionSort

private Sort exceptionSort

The Sort of the uncaught exception.

terminationKind

private IExecutionTermination.TerminationKind terminationKind

The TerminationKind.

Constructor Detail

ExecutionTermination

public ExecutionTermination(ITreeSettings settings,
                            Node proofNode,
                            IProgramVariable exceptionVariable,
                            IExecutionTermination.TerminationKind terminationKind)

Constructor.

Parameters:

settings - The ITreeSettings to use.

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

exceptionVariable - Contains the exception variable which is used to check if the executed program in proof terminates normally.

terminationKind - The TerminationKind or null to compute it when it is requested the first time (normal or exceptional termination only).

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.

getExceptionVariable

public IProgramVariable getExceptionVariable()

Returns the IProgramVariable which is used in the Sequent of Proof.root() to check if a normal or exceptional termination occurred.

Specified by:

getExceptionVariable in interface IExecutionTermination

Returns:

The IProgramVariable which is used to caught global exceptions.

getTerminationKind

public IExecutionTermination.TerminationKind getTerminationKind()

Returns the IExecutionTermination.TerminationKind.

Specified by:

getTerminationKind in interface IExecutionTermination

Returns:

The IExecutionTermination.TerminationKind.

isBlockContractTermination

protected boolean isBlockContractTermination()

Checks if a block contract terminates.

Returns:

true A block contract terminates, false normal execution terminates.

isExceptionalTermination

protected boolean isExceptionalTermination()

Checks if is an exceptional termination.

Returns:

true exceptional termination, false normal termination.

getExceptionSort

public Sort getExceptionSort()

Returns the Sort of the caught exception.

Specified by:

getExceptionSort in interface IExecutionTermination

Returns:

The Sort of the caught exception.

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.

isBranchVerified

public boolean isBranchVerified()

Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.

Specified by:

isBranchVerified in interface IExecutionTermination

Returns:

true verified/closed, false not verified/still open