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

Class ExecutionAuxiliaryContract

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode<SourceElement>

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

All Implemented Interfaces:

IExecutionAuxiliaryContract, IExecutionElement, IExecutionNode<SourceElement>

public class ExecutionAuxiliaryContract
extends AbstractExecutionNode<SourceElement>
implements IExecutionAuxiliaryContract

The default implementation of IExecutionAuxiliaryContract.

Author:

Martin Hentschel

Field Summary

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
ExecutionAuxiliaryContract(ITreeSettings settings, Node proofNode) Constructor.

Method Summary

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.

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

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

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

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

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

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

Constructor Detail

ExecutionAuxiliaryContract

public ExecutionAuxiliaryContract(ITreeSettings settings,
                                  Node proofNode)

Constructor.

Parameters:

settings - The ITreeSettings to use.

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

Method Detail

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.

lazyComputeConstraints

protected IExecutionConstraint[] lazyComputeConstraints()

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

Specified by:

lazyComputeConstraints in class AbstractExecutionNode<SourceElement>

Returns:

The IExecutionConstraints of the current state.

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

declaredVariableAsTerm

protected Term declaredVariableAsTerm(StatementBlock sb,
                                      int statementIndex)

Returns the variable declared by the statement at the given index as Term.

Parameters:

sb - The StatementBlock which contains all variable declarations.

statementIndex - The index in the StatementBlock with the variable declaration of interest.

Returns:

The variable as Term.

collectRemembranceVariables

protected void collectRemembranceVariables(Term term,
                                           java.util.Map<LocationVariable,Term> remembranceHeaps,
                                           java.util.Map<LocationVariable,Term> remembranceLocalVariables)

Collects recursive all remembrance variables.

Parameters:

term - The Term to start collecting.

remembranceHeaps - The Map to fill.

remembranceLocalVariables - The Map to fill.

isPreconditionComplied

public boolean isPreconditionComplied()

Checks if the precondition is complied.

Specified by:

isPreconditionComplied in interface IExecutionAuxiliaryContract

Returns:

true precondition complied, false precondition not complied.

getContract

public AuxiliaryContract getContract()

Returns the applied AuxiliaryContract.

Specified by:

getContract in interface IExecutionAuxiliaryContract

Returns:

The applied AuxiliaryContract.

getBlock

public StatementBlock getBlock()

Returns the StatementBlock at which the BlockContract is applied.

Specified by:

getBlock in interface IExecutionAuxiliaryContract

Returns:

The StatementBlock at which the BlockContract is applied.