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

Class ExecutionAllArrayIndicesVariable

java.lang.Object

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

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

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

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

All Implemented Interfaces:

IExecutionElement, IExecutionVariable

public class ExecutionAllArrayIndicesVariable
extends ExecutionVariable

An implementation of IExecutionVariable used to query all array indices at the same time. This supports also arrays where the length is symbolic and not a concrete number.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	ARRAY_INDEX_CONSTANT_NAME The name of the constant used to query the value of all array indices.
private Term	constant The constant representing an arbitrary array index.
static java.lang.String	NOT_A_VALUE_NAME The name used to represent the fact that a value is not available.
private Term	notAValue The constant representing the fact that no value is available.

Constructor Summary

Constructors

Constructor and Description
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, ExecutionValue parentValue, IProgramVariable arrayProgramVariable, Term additionalCondition) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	createArrayTerm() Creates a Term to access the array.
Term	createSelectTerm() Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().
Term	getConstant() Returns the constant representing an arbitrary array index.
Term	getNotAValue() Returns the constant representing the fact that no value is available.
protected boolean	isValidValue(Term value) Checks if the given Term represents a valid value.
protected java.lang.String	lazyComputeName() Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.
protected ExecutionValue[]	lazyComputeValues() Computes the value for ExecutionVariable.getValues() lazily when the method is called the first time.

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

computeValueCondition, getLengthValue, getParentNode, getParentValue, getValues, groupGoalsByValue, instantiateValuesFromSideProof

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

getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getProgramVariable, isArrayIndex

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

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

Field Detail

ARRAY_INDEX_CONSTANT_NAME

public static final java.lang.String ARRAY_INDEX_CONSTANT_NAME

The name of the constant used to query the value of all array indices.

See Also:

Constant Field Values

NOT_A_VALUE_NAME

public static final java.lang.String NOT_A_VALUE_NAME

The name used to represent the fact that a value is not available.

See Also:

Constant Field Values

constant

private Term constant

The constant representing an arbitrary array index.

notAValue

private final Term notAValue

The constant representing the fact that no value is available.

Constructor Detail

ExecutionAllArrayIndicesVariable

public ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
                                        Node proofNode,
                                        PosInOccurrence modalityPIO,
                                        ExecutionValue parentValue,
                                        IProgramVariable arrayProgramVariable,
                                        Term additionalCondition)

Constructor.

Parameters:

parentNode - The parent IExecutionNode.

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

modalityPIO - The PosInOccurrence of the modality of interest.

parentValue - The parent IExecutionValue representing the array.

arrayProgramVariable - The IProgramVariable of the array.

additionalCondition - An optional additional condition to consider.

Method Detail

lazyComputeName

protected java.lang.String lazyComputeName()
                                    throws ProofInputException

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

Overrides:

lazyComputeName in class AbstractExecutionVariable

Returns:

The human readable name of this IExecutionNode.

Throws:

ProofInputException

lazyComputeValues

protected ExecutionValue[] lazyComputeValues()
                                      throws ProofInputException

Computes the value for ExecutionVariable.getValues() lazily when the method is called the first time.

Overrides:

lazyComputeValues in class ExecutionVariable

Throws:

ProofInputException - Occurred Exception.

isValidValue

protected boolean isValidValue(Term value)

Checks if the given Term represents a valid value.

Overrides:

isValidValue in class ExecutionVariable

Parameters:

value - The value to check.

Returns:

true valid value, false invalid value to be ignored.

createArrayTerm

public Term createArrayTerm()

Creates a Term to access the array.

Returns:

The Term to access the array.

createSelectTerm

public Term createSelectTerm()

Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().

Specified by:

createSelectTerm in interface IExecutionVariable

Overrides:

createSelectTerm in class ExecutionVariable

Returns:

The created term.

getConstant

public Term getConstant()

Returns the constant representing an arbitrary array index.

Returns:

The constant representing an arbitrary array index.

getNotAValue

public Term getNotAValue()

Returns the constant representing the fact that no value is available.

Returns:

The constant representing the fact that no value is available.