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

Class AbstractExecutionVariable

java.lang.Object

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

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

All Implemented Interfaces:

IExecutionElement, IExecutionVariable

Direct Known Subclasses:

ExecutionVariable, ExecutionVariableExtractor.ExtractedExecutionVariable, ExecutionVariableExtractor.StateExecutionVariable

public abstract class AbstractExecutionVariable
extends AbstractExecutionElement
implements IExecutionVariable

Provides a basic implementation of IExecutionVariables.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	additionalCondition An optional additional condition to consider.
private Term	arrayIndex The index in the parent array.
private PosInOccurrence	modalityPIO The PosInOccurrence of the modality of interest.
private IExecutionValue	parentValue The parent ExecutionValue or null if not available.
private IProgramVariable	programVariable The represented IProgramVariable which value is shown.

Constructor Summary

Constructors

Constructor and Description
AbstractExecutionVariable(ITreeSettings settings, Node proofNode, IProgramVariable programVariable, IExecutionValue parentValue, Term arrayIndex, Term additionalCondition, PosInOccurrence modalityPIO) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	getAdditionalCondition() Returns the optional additional condition considered during value computation.
Term	getArrayIndex() Returns the index in the parent array if an array cell value is represented.
java.lang.String	getArrayIndexString() Returns the human readable index in the parent array if an array cell value is represented.
java.lang.String	getElementType() Returns a human readable element type name.
PosInOccurrence	getModalityPIO() Returns the PosInOccurrence of the modality of interest including updates.
IExecutionValue	getParentValue() Returns the parent IExecutionValue if available.
IProgramVariable	getProgramVariable() Returns the IProgramVariable which contains the represented value.
boolean	isArrayIndex() Checks if the current value is part of a parent array.
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.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.IExecutionVariable

createSelectTerm, getValues

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

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

Field Detail

programVariable

private final IProgramVariable programVariable

The represented IProgramVariable which value is shown.

parentValue

private final IExecutionValue parentValue

The parent ExecutionValue or null if not available.

arrayIndex

private final Term arrayIndex

The index in the parent array.

additionalCondition

private final Term additionalCondition

An optional additional condition to consider.

modalityPIO

private final PosInOccurrence modalityPIO

The PosInOccurrence of the modality of interest.

Constructor Detail

AbstractExecutionVariable

public AbstractExecutionVariable(ITreeSettings settings,
                                 Node proofNode,
                                 IProgramVariable programVariable,
                                 IExecutionValue parentValue,
                                 Term arrayIndex,
                                 Term additionalCondition,
                                 PosInOccurrence modalityPIO)

Constructor.

Parameters:

settings - The ITreeSettings to use.

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

programVariable - The represented IProgramVariable which value is shown.

parentValue - The parent IExecutionValue or null if not available.

arrayIndex - The index in the parent array.

additionalCondition - An optional additional condition to consider.

modalityPIO - The PosInOccurrence of the modality of interest.

Method Detail

getAdditionalCondition

public Term getAdditionalCondition()

Returns the optional additional condition considered during value computation.

Specified by:

getAdditionalCondition in interface IExecutionVariable

Returns:

The optional additional condition considered during value computation.

lazyComputeName

protected java.lang.String lazyComputeName()
                                    throws ProofInputException

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.

Throws:

ProofInputException

getProgramVariable

public IProgramVariable getProgramVariable()

Returns the IProgramVariable which contains the represented value.

Specified by:

getProgramVariable in interface IExecutionVariable

Returns:

The IProgramVariable which contains the represented value.

getArrayIndex

public Term getArrayIndex()

Returns the index in the parent array if an array cell value is represented.

Specified by:

getArrayIndex in interface IExecutionVariable

Returns:

The index in the parent array or null if no array cell value is represented.

getArrayIndexString

public java.lang.String getArrayIndexString()

Returns the human readable index in the parent array if an array cell value is represented.

Specified by:

getArrayIndexString in interface IExecutionVariable

Returns:

The human readable index in the parent array or null if no array cell value is represented.

isArrayIndex

public boolean isArrayIndex()

Checks if the current value is part of a parent array.

Specified by:

isArrayIndex in interface IExecutionVariable

Returns:

true is array cell value, false is a "normal" value.

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.

getParentValue

public IExecutionValue getParentValue()

Returns the parent IExecutionValue if available.

Specified by:

getParentValue in interface IExecutionVariable

Returns:

The parent IExecutionValue if available and null otherwise.

getModalityPIO

public PosInOccurrence getModalityPIO()

Returns the PosInOccurrence of the modality of interest including updates.

Specified by:

getModalityPIO in interface IExecutionElement

Returns:

The PosInOccurrence of the modality of interest including updates.