public abstract class AbstractExecutionValue extends AbstractExecutionElement implements IExecutionValue
IExecutionValue
.Modifier and Type | Field and Description |
---|---|
private Term |
condition
The condition under which the variable has this value.
|
private IExecutionConstraint[] |
constraints
The
IExecutionConstraint s. |
private Term |
value
The value.
|
private IExecutionVariable |
variable
The parent
IExecutionVariable which provides this IExecutionValue . |
Constructor and Description |
---|
AbstractExecutionValue(ITreeSettings settings,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected java.util.Set<Term> |
collectRelevantTerms(Services services,
Term term)
Collects all
Term s 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
IExecutionConstraint s. |
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
IExecutionConstraint s 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. |
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getChildVariables, getConditionString, getTypeString, getValueString, isValueUnknown
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final IExecutionVariable variable
IExecutionVariable
which provides this IExecutionValue
.private final Term condition
private IExecutionConstraint[] constraints
IExecutionConstraint
s.private final Term value
public AbstractExecutionValue(ITreeSettings settings, Node proofNode, IExecutionVariable variable, Term condition, Term value)
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.public IExecutionConstraint[] getConstraints() throws ProofInputException
IExecutionConstraint
s.getConstraints
in interface IExecutionValue
IExecutionConstraint
s.ProofInputException
- Occurred Exception.protected IExecutionConstraint[] lazyComputeConstraints() throws ProofInputException
getConstraints()
is called the first time.IExecutionConstraint
s.ProofInputException
- Occurred Exceptionprotected abstract IExecutionConstraint[] getNodeConstraints()
IExecutionConstraint
s of the IExecutionNode
on which this IExecutionValue
is part of.IExecutionConstraint
s.protected java.util.Set<Term> collectRelevantTerms(Services services, Term term)
Term
s contained in relevant constraints.protected void fillRelevantTerms(Services services, Term term, java.util.Set<Term> toFill)
collectRelevantTerms(Services, Term)
.protected boolean containsTerm(Term term, java.util.Set<Term> toSearch)
Term
contains at least one of the given once.public IExecutionVariable getVariable()
IExecutionVariable
.getVariable
in interface IExecutionValue
IExecutionVariable
.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public Term getCondition() throws ProofInputException
IExecutionValue.getVariable()
)
has this value.getCondition
in interface IExecutionValue
ProofInputException
- Occurred Exception.public Term getValue() throws ProofInputException
getValue
in interface IExecutionValue
ProofInputException
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.
isValueAnObject
in interface IExecutionValue
true
is an object, false
is an attribute of the object defined by the parent IExecutionValue
.ProofInputException
- Occurred Exception.