de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionAuxiliaryContract

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionAuxiliaryContract, ExecutionNodeReader.KeYlessBlockContract

public interface IExecutionAuxiliaryContract
extends IExecutionNode<SourceElement>

A node in the symbolic execution tree which represents a use block/loop contract application.

The default implementation is ExecutionAuxiliaryContract which is instantiated via a SymbolicExecutionTreeBuilder instance.

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionAuxiliaryContract

Field Summary

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

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Method Summary

Modifier and Type	Method and Description
StatementBlock	getBlock() Returns the StatementBlock at which the BlockContract is applied.
AuxiliaryContract	getContract() Returns the applied AuxiliaryContract.
boolean	isPreconditionComplied() Checks if the precondition is complied.

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, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Method Detail

getContract

AuxiliaryContract getContract()

Returns the applied AuxiliaryContract.

Returns:

The applied AuxiliaryContract.

getBlock

StatementBlock getBlock()

Returns the StatementBlock at which the BlockContract is applied.

Returns:

The StatementBlock at which the BlockContract is applied.

isPreconditionComplied

boolean isPreconditionComplied()

Checks if the precondition is complied.

Returns:

true precondition complied, false precondition not complied.