de.uka.ilkd.key.symbolic_execution.po

Class ProgramMethodPO

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractPO

de.uka.ilkd.key.proof.init.AbstractOperationPO

de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO

All Implemented Interfaces:

IPersistablePO, ProofOblInput

Direct Known Subclasses:

ProgramMethodSubsetPO

public class ProgramMethodPO
extends AbstractOperationPO

This proof obligation executes an IProgramMethod with an optional precondition.

The generated Sequent has the following form:

 
 ==>
 <generalAssumptions> &
 <preconditions>
 ->
 <updatesToStoreInitialValues>
 <modalityStart>
 exc=null;try {<methodBodyStatement>}catch(java.lang.Exception e) {exc = e}
 <modalityEnd>
 (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
 
 

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.proof.init.IPersistablePO

IPersistablePO.LoadedPOContainer

Field Summary

Fields

Modifier and Type	Field and Description
private IProgramMethod	pm The IProgramMethod to execute code parts from.
private java.lang.String	precondition The precondition in JML syntax.

Fields inherited from class de.uka.ilkd.key.proof.init.AbstractOperationPO

proofConfig

Fields inherited from class de.uka.ilkd.key.proof.init.AbstractPO

environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb

Fields inherited from interface de.uka.ilkd.key.proof.init.IPersistablePO

PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME

Constructor Summary

Constructors

Constructor and Description
ProgramMethodPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition) Constructor.
ProgramMethodPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition, boolean addUninterpretedPredicate, boolean addSymbolicExecutionLabel) Constructor.

Method Summary

Modifier and Type	Method and Description
protected Term	buildFrameClause(java.util.List<LocationVariable> modHeaps, java.util.Map<Term,Term> heapToAtPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) Builds the frame clause including the modifies clause.
protected ImmutableList<StatementBlock>	buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services) Builds the code to execute in different statement blocks. 1. code to execute before the try block 2. code to execute in the try block 3. code to execute in the catch block 4. code to execute in the finally block
protected java.lang.String	buildPOName(boolean transactionFlag) Returns the name of the Proof based on the given transaction flag.
boolean	equals(java.lang.Object obj)
void	fillSaveProperties(java.util.Properties properties) This method is called by a ProofSaver to store the proof specific settings in the given Properties.
protected Term	generateMbyAtPreDef(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
protected KeYJavaType	getCalleeKeYJavaType() Returns the KeYJavaType which contains AbstractOperationPO.getProgramMethod().
KeYJavaType	getContainerType() Returns the KeYJavaType in which the proven element is contained in.
protected Term	getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
protected Term	getPost(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services) Creates the postcondition.
protected Term	getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services) Creates the precondition.
java.lang.String	getPrecondition() Returns the precondition in JML syntax.
static java.lang.String	getPrecondition(java.util.Properties properties) Returns the optional defined precondition.
IProgramMethod	getProgramMethod() Returns the IProgramMethod to call.
static IProgramMethod	getProgramMethod(InitConfig initConfig, java.util.Properties properties) Searches the IProgramMethod defined by the given Properties.
static java.lang.String	getProgramMethodSignature(IProgramMethod pm, boolean includeType) Returns a human readable full qualified method signature.
protected Modality	getTerminationMarker() Returns the Modality to use as termination marker.
int	hashCode()
protected boolean	isCopyOfMethodArgumentsUsed() Checks if a copy of the method call arguments are used instead of the original method arguments.
protected boolean	isMakeNamesUnique() Checks if self variable, exception variable, result variable and method call arguments should be renamed to make sure that their names are unique in the whole KeY application.
protected boolean	isTransactionApplicable() Checks if transactions are applicable.
static IPersistablePO.LoadedPOContainer	loadFrom(InitConfig initConfig, java.util.Properties properties) Instantiates a new proof obligation with the given settings.

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractOperationPO

addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFreePre, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit, readProblem

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractPO

assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getName, getPO, implies, name, register, register, register, selectClassAxioms

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Field Detail

pm

private IProgramMethod pm

The IProgramMethod to execute code parts from.

precondition

private java.lang.String precondition

The precondition in JML syntax.

Constructor Detail

ProgramMethodPO

public ProgramMethodPO(InitConfig initConfig,
                       java.lang.String name,
                       IProgramMethod pm,
                       java.lang.String precondition)

Constructor.

Parameters:

initConfig - The InitConfig to use.

name - The name to use.

pm - The IProgramMethod to execute code parts from.

precondition - An optional precondition to use.

ProgramMethodPO

public ProgramMethodPO(InitConfig initConfig,
                       java.lang.String name,
                       IProgramMethod pm,
                       java.lang.String precondition,
                       boolean addUninterpretedPredicate,
                       boolean addSymbolicExecutionLabel)

Constructor.

Parameters:

initConfig - The InitConfig to use.

name - The name to use.

pm - The IProgramMethod to execute code parts from.

precondition - An optional precondition to use.

addUninterpretedPredicate - true postcondition contains uninterpreted predicate, false uninterpreted predicate is not contained in postcondition.

addSymbolicExecutionLabel - true to add the SymbolicExecutionTermLabel to the modality, false to not label the modality.

Method Detail

getProgramMethod

public IProgramMethod getProgramMethod()

Returns the IProgramMethod to call.

Specified by:

getProgramMethod in class AbstractOperationPO

Returns:

The IProgramMethod to call.

isTransactionApplicable

protected boolean isTransactionApplicable()

Checks if transactions are applicable.

Specified by:

isTransactionApplicable in class AbstractOperationPO

Returns:

Transactions are applicable?

getCalleeKeYJavaType

protected KeYJavaType getCalleeKeYJavaType()

Returns the KeYJavaType which contains AbstractOperationPO.getProgramMethod().

Specified by:

getCalleeKeYJavaType in class AbstractOperationPO

Returns:

The KeYJavaType which contains AbstractOperationPO.getProgramMethod().

buildOperationBlocks

protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
                                                             ProgramVariable selfVar,
                                                             ProgramVariable resultVar,
                                                             Services services)

Builds the code to execute in different statement blocks. 1. code to execute before the try block 2. code to execute in the try block 3. code to execute in the catch block 4. code to execute in the finally block

Specified by:

buildOperationBlocks in class AbstractOperationPO

Parameters:

formalParVars - Arguments from formal parameters for method call.

selfVar - The self variable.

resultVar - The result variable.

services - services instance

Returns:

operation blocks as statement blocks

generateMbyAtPreDef

protected Term generateMbyAtPreDef(ProgramVariable selfVar,
                                   ImmutableList<ProgramVariable> paramVars,
                                   Services services)

Specified by:

generateMbyAtPreDef in class AbstractOperationPO

getPre

protected Term getPre(java.util.List<LocationVariable> modHeaps,
                      ProgramVariable selfVar,
                      ImmutableList<ProgramVariable> paramVars,
                      java.util.Map<LocationVariable,LocationVariable> atPreVars,
                      Services services)

Creates the precondition.

Specified by:

getPre in class AbstractOperationPO

Parameters:

modHeaps - The heaps.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

atPreVars - Mapping of LocationVariable to the LocationVariable which contains the initial value.

services - The Services to use.

Returns:

The Term representing the precondition.

getPost

protected Term getPost(java.util.List<LocationVariable> modHeaps,
                       ProgramVariable selfVar,
                       ImmutableList<ProgramVariable> paramVars,
                       ProgramVariable resultVar,
                       ProgramVariable exceptionVar,
                       java.util.Map<LocationVariable,LocationVariable> atPreVars,
                       Services services)

Creates the postcondition.

Specified by:

getPost in class AbstractOperationPO

Parameters:

modHeaps - The heaps.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

resultVar - The result variable.

exceptionVar - The exception variable.

atPreVars - Mapping of LocationVariable to the LocationVariable which contains the initial value.

services - The Services to use.

Returns:

The Term representing the postcondition.

buildFrameClause

protected Term buildFrameClause(java.util.List<LocationVariable> modHeaps,
                                java.util.Map<Term,Term> heapToAtPre,
                                ProgramVariable selfVar,
                                ImmutableList<ProgramVariable> paramVars,
                                Services services)

Builds the frame clause including the modifies clause.

Specified by:

buildFrameClause in class AbstractOperationPO

Parameters:

modHeaps - The heaps.

heapToAtPre - The previous heap before execution.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

services - services instance

Returns:

The created Term representing the frame clause.

getTerminationMarker

protected Modality getTerminationMarker()

Returns the Modality to use as termination marker.

Specified by:

getTerminationMarker in class AbstractOperationPO

Returns:

The Modality to use as termination marker.

isMakeNamesUnique

protected boolean isMakeNamesUnique()

Checks if self variable, exception variable, result variable and method call arguments should be renamed to make sure that their names are unique in the whole KeY application.

Overrides:

isMakeNamesUnique in class AbstractOperationPO

Returns:

true use unique names, false use original names even if they are not unique in whole KeY application.

isCopyOfMethodArgumentsUsed

protected boolean isCopyOfMethodArgumentsUsed()

Checks if a copy of the method call arguments are used instead of the original method arguments.

Overrides:

isCopyOfMethodArgumentsUsed in class AbstractOperationPO

Returns:

true use copy of method call arguments, false use original method call arguments.

buildPOName

protected java.lang.String buildPOName(boolean transactionFlag)

Returns the name of the Proof based on the given transaction flag.

Specified by:

buildPOName in class AbstractOperationPO

Parameters:

transactionFlag - The transaction flag.

Returns:

The proof name to use.

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

getPrecondition

public java.lang.String getPrecondition()

Returns the precondition in JML syntax.

Returns:

The precondition in JML syntax.

fillSaveProperties

public void fillSaveProperties(java.util.Properties properties)
                        throws java.io.IOException

This method is called by a ProofSaver to store the proof specific settings in the given Properties. The stored settings have to contain all information required to instantiate the proof obligation again and this instance should create the same Sequent (if code and specifications are unchanged).

Specified by:

fillSaveProperties in interface IPersistablePO

Overrides:

fillSaveProperties in class AbstractOperationPO

Parameters:

properties - The Properties to fill with the proof obligation specific settings.

Throws:

java.io.IOException - Occurred Exception.

getProgramMethodSignature

public static java.lang.String getProgramMethodSignature(IProgramMethod pm,
                                                         boolean includeType)
                                                  throws java.io.IOException

Returns a human readable full qualified method signature.

Parameters:

pm - The IProgramMethod which provides the signature.

includeType - Include the container type?

Returns:

The human readable method signature.

Throws:

java.io.IOException - Occurred Exception.

loadFrom

public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig,
                                                        java.util.Properties properties)
                                                 throws java.io.IOException

Instantiates a new proof obligation with the given settings.

Parameters:

initConfig - The already load InitConfig.

properties - The settings of the proof obligation to instantiate.

Returns:

The instantiated proof obligation.

Throws:

java.io.IOException - Occurred Exception.

getProgramMethod

public static IProgramMethod getProgramMethod(InitConfig initConfig,
                                              java.util.Properties properties)
                                       throws java.io.IOException

Searches the IProgramMethod defined by the given Properties.

Parameters:

initConfig - The already load InitConfig.

properties - The settings of the proof obligation to instantiate.

Returns:

The found IProgramMethod.

Throws:

java.io.IOException - Occurred Exception if it was not possible to find the IProgramMethod.

getPrecondition

public static java.lang.String getPrecondition(java.util.Properties properties)

Returns the optional defined precondition.

Parameters:

properties - The proof obligation settings to read from.

Returns:

The precondition or null if not available.

getGlobalDefs

protected Term getGlobalDefs(LocationVariable heap,
                             Term heapTerm,
                             Term selfTerm,
                             ImmutableList<Term> paramTerms,
                             Services services)

Specified by:

getGlobalDefs in class AbstractOperationPO

getContainerType

public KeYJavaType getContainerType()

Returns the KeYJavaType in which the proven element is contained in.

Specified by:

getContainerType in interface ProofOblInput

Overrides:

getContainerType in class AbstractPO

Returns:

The KeYJavaType in which the proven element is contained in or null if not available.