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

Class AbstractExecutionValue

java.lang.Object

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

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

All Implemented Interfaces:

IExecutionElement, IExecutionValue

Direct Known Subclasses:

ExecutionValue, ExecutionVariableExtractor.ExtractedExecutionValue

public abstract class AbstractExecutionValue
extends AbstractExecutionElement
implements IExecutionValue

Provides a basic implementation of IExecutionValue.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	condition The condition under which the variable has this value.
private IExecutionConstraint[]	constraints The IExecutionConstraints.
private Term	value The value.
private IExecutionVariable	variable The parent IExecutionVariable which provides this IExecutionValue.

Constructor Summary

Constructors

Constructor and Description
AbstractExecutionValue(ITreeSettings settings, Node proofNode, IExecutionVariable variable, Term condition, Term value) Constructor.

Method Summary

Modifier and Type	Method and Description
protected java.util.Set<Term>	collectRelevantTerms(Services services, Term term) Collects all Terms contained in relevant constraints.
protected boolean	containsTerm(Term term, java.util.Set<Term> toSearch) Checks if the given Term contains at least one of the given once.
protected void	fillRelevantTerms(Services services, Term term, java.util.Set<Term> toFill) Utility method used by collectRelevantTerms(Services, Term).
Term	getCondition() Returns the condition under which the variable (IExecutionValue.getVariable()) has this value.
IExecutionConstraint[]	getConstraints() Returns all available IExecutionConstraints.
java.lang.String	getElementType() Returns a human readable element type name.
PosInOccurrence	getModalityPIO() Returns the PosInOccurrence of the modality of interest including updates.
protected abstract IExecutionConstraint[]	getNodeConstraints() Returns all available IExecutionConstraints of the IExecutionNode on which this IExecutionValue is part of.
Term	getValue() Returns the value of the variable.
IExecutionVariable	getVariable() Returns the parent IExecutionVariable.
boolean	isValueAnObject() Checks if the value represents an object or an attribute of the object defined by the parent IExecutionValue.
protected IExecutionConstraint[]	lazyComputeConstraints() Computes the related constraints lazily when 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.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.IExecutionValue

getChildVariables, getConditionString, getTypeString, getValueString, isValueUnknown

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

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

Field Detail

variable

private final IExecutionVariable variable

The parent IExecutionVariable which provides this IExecutionValue.

condition

private final Term condition

The condition under which the variable has this value.

constraints

private IExecutionConstraint[] constraints

The IExecutionConstraints.

value

private final Term value

The value.

Constructor Detail

AbstractExecutionValue

public AbstractExecutionValue(ITreeSettings settings,
                              Node proofNode,
                              IExecutionVariable variable,
                              Term condition,
                              Term value)

Constructor.

Parameters:

settings - The ITreeSettings to use.

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

variable - The parent IExecutionVariable which contains this value.

condition - The condition.

value - The value.

Method Detail

getConstraints

public IExecutionConstraint[] getConstraints()
                                      throws ProofInputException

Returns all available IExecutionConstraints.

Specified by:

getConstraints in interface IExecutionValue

Returns:

The available IExecutionConstraints.

Throws:

ProofInputException - Occurred Exception.

lazyComputeConstraints

protected IExecutionConstraint[] lazyComputeConstraints()
                                                 throws ProofInputException

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

Returns:

The related IExecutionConstraints.

Throws:

ProofInputException - Occurred Exception

getNodeConstraints

protected abstract IExecutionConstraint[] getNodeConstraints()

Returns all available IExecutionConstraints of the IExecutionNode on which this IExecutionValue is part of.

Returns:

All available IExecutionConstraints.

collectRelevantTerms

protected java.util.Set<Term> collectRelevantTerms(Services services,
                                                   Term term)

Collects all Terms contained in relevant constraints.

Parameters:

services - The Services to use.

term - The initial Term.

Returns:

The relevant Terms.

fillRelevantTerms

protected void fillRelevantTerms(Services services,
                                 Term term,
                                 java.util.Set<Term> toFill)

Utility method used by collectRelevantTerms(Services, Term).

Parameters:

services - The Services to use.

term - The initial Term.

toFill - The Set of relevant Terms to fill.

containsTerm

protected boolean containsTerm(Term term,
                               java.util.Set<Term> toSearch)

Checks if the given Term contains at least one of the given once.

Parameters:

term - The Term to search in.

toSearch - The Terms to search.

Returns:

true at least one Term is contained, false none of the Terms is contained.

getVariable

public IExecutionVariable getVariable()

Returns the parent IExecutionVariable.

Specified by:

getVariable in interface IExecutionValue

Returns:

The parent IExecutionVariable.

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.

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

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.

getCondition

public Term getCondition()
                  throws ProofInputException

Returns the condition under which the variable (IExecutionValue.getVariable()) has this value.

Specified by:

getCondition in interface IExecutionValue

Returns:

The condition.

Throws:

ProofInputException - Occurred Exception.

getValue

public Term getValue()
              throws ProofInputException

Returns the value of the variable.

Specified by:

getValue in interface IExecutionValue

Returns:

The value of the variable.

Throws:

ProofInputException

isValueAnObject

public boolean isValueAnObject()
                        throws ProofInputException

Checks if the value represents an object or an attribute of the object defined by the parent IExecutionValue.

All values which are not a basic datatype (integer, boolean, ...) and not an instance of a library class will be treated as object.

Specified by:

isValueAnObject in interface IExecutionValue

Returns:

true is an object, false is an attribute of the object defined by the parent IExecutionValue.

Throws:

ProofInputException - Occurred Exception.