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

Class AbstractExecutionElement

java.lang.Object

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

All Implemented Interfaces:

IExecutionElement

Direct Known Subclasses:

AbstractExecutionNode, AbstractExecutionValue, AbstractExecutionVariable, ExecutionConstraint, ExecutionMethodReturnValue

public abstract class AbstractExecutionElement
extends java.lang.Object
implements IExecutionElement

Provides a basic implementation of IExecutionElement.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	name The human readable name of this node.
private Node	proofNode The Node of KeY's proof tree which is represented by this IExecutionNode.
private ITreeSettings	settings The used TreeSettings.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
protected java.lang.String	formatTerm(Term term, Services services) Converts the given Term into a String respecting #isUsePretty().
RuleApp	getAppliedRuleApp() Returns the applied RuleApp.
InitConfig	getInitConfig() Returns the InitConfig used by IExecutionElement.getProof().
java.lang.String	getName() Returns a human readable name which describes this element.
Proof	getProof() Returns the Proof from which the symbolic execution tree was extracted.
Node	getProofNode() Returns the Node in KeY's proof tree which is represented by this execution tree node.
NodeInfo	getProofNodeInfo() Returns the NodeInfo of IExecutionElement.getProofNode().
Services	getServices() Returns the Services used by IExecutionElement.getProof().
ITreeSettings	getSettings() Returns the ITreeSettings to use.
boolean	isDisposed() Checks if the proof is disposed.
protected boolean	isNameComputed() Checks if the value of getName() is already computed.
protected abstract java.lang.String	lazyComputeName() Computes the name of this node lazily when getName() is called the first time.
protected void	setName(java.lang.String name) Sets the name.
java.lang.String	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.IExecutionElement

getElementType, getModalityPIO

Field Detail

settings

private final ITreeSettings settings

The used TreeSettings.

proofNode

private final Node proofNode

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

name

private java.lang.String name

The human readable name of this node.

Constructor Detail

AbstractExecutionElement

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

getServices

public Services getServices()

Returns the Services used by IExecutionElement.getProof().

Specified by:

getServices in interface IExecutionElement

Returns:

The Services used by IExecutionElement.getProof().

getAppliedRuleApp

public RuleApp getAppliedRuleApp()

Returns the applied RuleApp.

Specified by:

getAppliedRuleApp in interface IExecutionElement

Returns:

The applied RuleApp.

getInitConfig

public InitConfig getInitConfig()

Returns the InitConfig used by IExecutionElement.getProof().

Specified by:

getInitConfig in interface IExecutionElement

Returns:

The InitConfig used by IExecutionElement.getProof().

getProof

public Proof getProof()

Returns the Proof from which the symbolic execution tree was extracted.

Specified by:

getProof in interface IExecutionElement

Returns:

The Proof from which the symbolic execution tree was extracted.

getProofNode

public Node getProofNode()

Returns the Node in KeY's proof tree which is represented by this execution tree node.

Specified by:

getProofNode in interface IExecutionElement

Returns:

The Node in KeY's proof tree which is represented by this execution tree node.

getProofNodeInfo

public NodeInfo getProofNodeInfo()

Returns the NodeInfo of IExecutionElement.getProofNode().

Specified by:

getProofNodeInfo in interface IExecutionElement

Returns:

The NodeInfo of IExecutionElement.getProofNode().

getName

public java.lang.String getName()
                         throws ProofInputException

Returns a human readable name which describes this element.

Specified by:

getName in interface IExecutionElement

Returns:

The human readable name which describes this element.

Throws:

ProofInputException - Occurred Exception.

setName

protected void setName(java.lang.String name)

Sets the name.

Parameters:

name - The new name to set.

isNameComputed

protected boolean isNameComputed()

Checks if the value of getName() is already computed.

Returns:

ture name is computed, false name is not computed yet.

lazyComputeName

protected abstract java.lang.String lazyComputeName()
                                             throws ProofInputException

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

Returns:

The human readable name of this IExecutionNode.

Throws:

ProofInputException

formatTerm

protected java.lang.String formatTerm(Term term,
                                      Services services)

Converts the given Term into a String respecting #isUsePretty().

Parameters:

term - The Term to convert.

services - The Services to use.

Returns:

The String representation of the given Term.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

isDisposed

public boolean isDisposed()

Checks if the proof is disposed.

Specified by:

isDisposed in interface IExecutionElement

Returns:

true proof is disposed, false proof is not disposed and still valid.

getSettings

public ITreeSettings getSettings()

Returns the ITreeSettings to use.

Specified by:

getSettings in interface IExecutionElement

Returns:

The ITreeSettings to use.