de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionOperationContract

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionNodeReader.KeYlessOperationContract, ExecutionOperationContract

public interface IExecutionOperationContract
extends IExecutionNode<SourceElement>

A node in the symbolic execution tree which represents a use operation contract application.

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

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionOperationContract

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
Contract	getContract() Returns the applied Contract.
ImmutableList<Term>	getContractParams() Returns the parameters of the called method for which a Contract is applied.
IProgramMethod	getContractProgramMethod() Returns the IProgramMethod of the applied Contract.
Term	getExceptionTerm() Returns the exception Term in which a by the Contract thrown Exception is stored.
java.lang.String	getFormatedContractParams() Returns the human readable parameters of the called method for which a Contract is applied.
java.lang.String	getFormatedExceptionTerm() Returns the human readable exception Term in which a by the Contract thrown Exception is stored.
java.lang.String	getFormatedResultTerm() Returns the human readable result Term in which the result of the applied Contract is stored.
java.lang.String	getFormatedSelfTerm() Returns the human readable self Term of the called method for which a Contract is applied.
Term	getResultTerm() Returns the result Term in which the result of the applied Contract is stored.
Term	getSelfTerm() Returns the self Term of the called method for which a Contract is applied.
boolean	hasNotNullCheck() Checks if a not null check is available (instance method) or not (static method or constructor).
boolean	isNotNullCheckComplied() Checks if the not null check is complied.
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

Contract getContract()

Returns the applied Contract.

Returns:

The applied Contract.

getContractProgramMethod

IProgramMethod getContractProgramMethod()

Returns the IProgramMethod of the applied Contract.

Returns:

The IProgramMethod of the applied Contract.

isPreconditionComplied

boolean isPreconditionComplied()

Checks if the precondition is complied.

Returns:

true precondition complied, false precondition not complied.

hasNotNullCheck

boolean hasNotNullCheck()

Checks if a not null check is available (instance method) or not (static method or constructor).

Returns:

true not null check available, false not null check is not available.

isNotNullCheckComplied

boolean isNotNullCheckComplied()

Checks if the not null check is complied.

Returns:

true not null check complied, false not null check not complied.

getResultTerm

Term getResultTerm()
            throws ProofInputException

Returns the result Term in which the result of the applied Contract is stored.

Returns:

The result Term in which the result of the applied Contract is stored.

Throws:

ProofInputException - Occurred Exception.

getExceptionTerm

Term getExceptionTerm()
               throws ProofInputException

Returns the exception Term in which a by the Contract thrown Exception is stored.

Returns:

The exception Term in which a by the Contract thrown Exception is stored.

Throws:

ProofInputException - Occurred Exception.

getSelfTerm

Term getSelfTerm()
          throws ProofInputException

Returns the self Term of the called method for which a Contract is applied.

Returns:

The self Term or null if not available.

Throws:

ProofInputException - Occurred Exception.

getContractParams

ImmutableList<Term> getContractParams()
                               throws ProofInputException

Returns the parameters of the called method for which a Contract is applied.

Returns:

The parameters of the called method for which a Contract is applied.

Throws:

ProofInputException - Occurred Exception.

getFormatedResultTerm

java.lang.String getFormatedResultTerm()
                                throws ProofInputException

Returns the human readable result Term in which the result of the applied Contract is stored.

Returns:

The human readable result Term in which the result of the applied Contract is stored.

Throws:

ProofInputException - Occurred Exception.

getFormatedExceptionTerm

java.lang.String getFormatedExceptionTerm()
                                   throws ProofInputException

Returns the human readable exception Term in which a by the Contract thrown Exception is stored.

Returns:

The human readable exception Term in which a by the Contract thrown Exception is stored.

Throws:

ProofInputException - Occurred Exception.

getFormatedSelfTerm

java.lang.String getFormatedSelfTerm()
                              throws ProofInputException

Returns the human readable self Term of the called method for which a Contract is applied.

Returns:

The human readable self Term or null if not available.

Throws:

ProofInputException - Occurred Exception.

getFormatedContractParams

java.lang.String getFormatedContractParams()
                                    throws ProofInputException

Returns the human readable parameters of the called method for which a Contract is applied.

Returns:

The human readable parameters of the called method for which a Contract is applied.

Throws:

ProofInputException - Occurred Exception.