public class ExecutionAuxiliaryContract extends AbstractExecutionNode<SourceElement> implements IExecutionAuxiliaryContract
IExecutionAuxiliaryContract
.INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionAuxiliaryContract(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected void |
collectRemembranceVariables(Term term,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables)
Collects recursive all remembrance variables.
|
protected Term |
declaredVariableAsTerm(StatementBlock sb,
int statementIndex)
Returns the variable declared by the statement at the given index as
Term . |
StatementBlock |
getBlock()
Returns the
StatementBlock at which the BlockContract is applied. |
AuxiliaryContract |
getContract()
Returns the applied
AuxiliaryContract . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.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. |
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
public ExecutionAuxiliaryContract(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
protected Term declaredVariableAsTerm(StatementBlock sb, int statementIndex)
Term
.sb
- The StatementBlock
which contains all variable declarations.statementIndex
- The index in the StatementBlock
with the variable declaration of interest.Term
.protected void collectRemembranceVariables(Term term, java.util.Map<LocationVariable,Term> remembranceHeaps, java.util.Map<LocationVariable,Term> remembranceLocalVariables)
term
- The Term
to start collecting.remembranceHeaps
- The Map
to fill.remembranceLocalVariables
- The Map
to fill.public boolean isPreconditionComplied()
isPreconditionComplied
in interface IExecutionAuxiliaryContract
true
precondition complied, false
precondition not complied.public AuxiliaryContract getContract()
AuxiliaryContract
.getContract
in interface IExecutionAuxiliaryContract
AuxiliaryContract
.public StatementBlock getBlock()
StatementBlock
at which the BlockContract
is applied.getBlock
in interface IExecutionAuxiliaryContract
StatementBlock
at which the BlockContract
is applied.