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

Class ExecutionOperationContract

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

All Implemented Interfaces:

IExecutionElement, IExecutionNode<SourceElement>, IExecutionOperationContract

public class ExecutionOperationContract
extends AbstractExecutionNode<SourceElement>
implements IExecutionOperationContract

The default implementation of IExecutionOperationContract.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<Term>	contractParams The current contract parameters.
private Term	exceptionTerm The exception Term used by the applied Contract.
private Term	resultTerm The result Term used by the applied Contract.
private Term	selfTerm The self Term or null if not available.

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
ExecutionOperationContract(ITreeSettings settings, Node proofNode) Constructor.

Method Summary

Modifier and Type	Method and Description
protected static LocationVariable	extractResultVariableFromPostBranch(Node node, Services services) Extracts the result variable from the given post branch.
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.
java.lang.String	getElementType() Returns a human readable element type name.
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.
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.
protected Term	searchConstructorSelfDefinition(Term term, KeYJavaType staticType, Services services) Tries to find the self Term of the given KeYJavaType.
protected Term	searchResultTerm(FunctionalOperationContract contract, UseOperationContractRule.Instantiation inst, Services services) Searches the result Term.

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

Field Detail

exceptionTerm

private Term exceptionTerm

The exception Term used by the applied Contract.

resultTerm

private Term resultTerm

The result Term used by the applied Contract.

selfTerm

private Term selfTerm

The self Term or null if not available.

contractParams

private ImmutableList<Term> contractParams

The current contract parameters.

Constructor Detail

ExecutionOperationContract

public ExecutionOperationContract(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

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

searchConstructorSelfDefinition

protected Term searchConstructorSelfDefinition(Term term,
                                               KeYJavaType staticType,
                                               Services services)

Tries to find the self Term of the given KeYJavaType.

Parameters:

term - The Term to start search in.

staticType - The expected KeYJavaType.

services - The Services to use.

Returns:

The found self Term or null if not available.

getResultTerm

public Term getResultTerm()
                   throws ProofInputException

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

Specified by:

getResultTerm in interface IExecutionOperationContract

Returns:

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

Throws:

ProofInputException - Occurred Exception.

getExceptionTerm

public Term getExceptionTerm()
                      throws ProofInputException

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

Specified by:

getExceptionTerm in interface IExecutionOperationContract

Returns:

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

Throws:

ProofInputException - Occurred Exception.

getSelfTerm

public Term getSelfTerm()
                 throws ProofInputException

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

Specified by:

getSelfTerm in interface IExecutionOperationContract

Returns:

The self Term or null if not available.

Throws:

ProofInputException - Occurred Exception.

getContractParams

public ImmutableList<Term> getContractParams()
                                      throws ProofInputException

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

Specified by:

getContractParams in interface IExecutionOperationContract

Returns:

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

Throws:

ProofInputException - Occurred Exception.

getFormatedResultTerm

public java.lang.String getFormatedResultTerm()
                                       throws ProofInputException

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

Specified by:

getFormatedResultTerm in interface IExecutionOperationContract

Returns:

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

Throws:

ProofInputException - Occurred Exception.

getFormatedExceptionTerm

public java.lang.String getFormatedExceptionTerm()
                                          throws ProofInputException

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

Specified by:

getFormatedExceptionTerm in interface IExecutionOperationContract

Returns:

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

Throws:

ProofInputException - Occurred Exception.

getFormatedSelfTerm

public java.lang.String getFormatedSelfTerm()
                                     throws ProofInputException

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

Specified by:

getFormatedSelfTerm in interface IExecutionOperationContract

Returns:

The human readable self Term or null if not available.

Throws:

ProofInputException - Occurred Exception.

getFormatedContractParams

public java.lang.String getFormatedContractParams()
                                           throws ProofInputException

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

Specified by:

getFormatedContractParams in interface IExecutionOperationContract

Returns:

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

Throws:

ProofInputException - Occurred Exception.

searchResultTerm

protected Term searchResultTerm(FunctionalOperationContract contract,
                                UseOperationContractRule.Instantiation inst,
                                Services services)

Searches the result Term.

Parameters:

contract - The FunctionalOperationContract.

inst - The UseOperationContractRule.Instantiation.

services - The Services.

Returns:

The found result Term or null otherwise.

extractResultVariableFromPostBranch

protected static LocationVariable extractResultVariableFromPostBranch(Node node,
                                                                      Services services)

Extracts the result variable from the given post branch.

Parameters:

node - The Node which is the post or exceptional post branch of an applied ContractRuleApp.

services - The Services to use.

Returns:

The found LocationVariable or null if not found.

getContract

public Contract getContract()

Returns the applied Contract.

Specified by:

getContract in interface IExecutionOperationContract

Returns:

The applied Contract.

getContractProgramMethod

public IProgramMethod getContractProgramMethod()

Returns the IProgramMethod of the applied Contract.

Specified by:

getContractProgramMethod in interface IExecutionOperationContract

Returns:

The IProgramMethod of the applied Contract.

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.

isPreconditionComplied

public boolean isPreconditionComplied()

Checks if the precondition is complied.

Specified by:

isPreconditionComplied in interface IExecutionOperationContract

Returns:

true precondition complied, false precondition not complied.

hasNotNullCheck

public boolean hasNotNullCheck()

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

Specified by:

hasNotNullCheck in interface IExecutionOperationContract

Returns:

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

isNotNullCheckComplied

public boolean isNotNullCheckComplied()

Checks if the not null check is complied.

Specified by:

isNotNullCheckComplied in interface IExecutionOperationContract

Returns:

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