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>)
IPersistablePO.LoadedPOContainer
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.
|
proofConfig
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
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.
|
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.
|
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
assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getName, getPO, implies, name, register, register, register, selectClassAxioms
private IProgramMethod pm
IProgramMethod
to execute code parts from.private java.lang.String precondition
public ProgramMethodPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition)
initConfig
- The InitConfig
to use.name
- The name to use.pm
- The IProgramMethod
to execute code parts from.precondition
- An optional precondition to use.public ProgramMethodPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition, boolean addUninterpretedPredicate, boolean addSymbolicExecutionLabel)
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.public IProgramMethod getProgramMethod()
IProgramMethod
to call.getProgramMethod
in class AbstractOperationPO
IProgramMethod
to call.protected boolean isTransactionApplicable()
isTransactionApplicable
in class AbstractOperationPO
protected KeYJavaType getCalleeKeYJavaType()
KeYJavaType
which contains AbstractOperationPO.getProgramMethod()
.getCalleeKeYJavaType
in class AbstractOperationPO
KeYJavaType
which contains AbstractOperationPO.getProgramMethod()
.protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services)
buildOperationBlocks
in class AbstractOperationPO
formalParVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.services
- services instanceprotected Term generateMbyAtPreDef(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
generateMbyAtPreDef
in class AbstractOperationPO
protected Term getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
getPre
in class AbstractOperationPO
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the precondition.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)
getPost
in class AbstractOperationPO
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.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.Term
representing the postcondition.protected Term buildFrameClause(java.util.List<LocationVariable> modHeaps, java.util.Map<Term,Term> heapToAtPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
buildFrameClause
in class AbstractOperationPO
modHeaps
- The heaps.heapToAtPre
- The previous heap before execution.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.services
- services instanceTerm
representing the frame clause.protected Modality getTerminationMarker()
Modality
to use as termination marker.getTerminationMarker
in class AbstractOperationPO
Modality
to use as termination marker.protected boolean isMakeNamesUnique()
isMakeNamesUnique
in class AbstractOperationPO
true
use unique names, false
use original
names even if they are not unique in whole KeY application.protected boolean isCopyOfMethodArgumentsUsed()
isCopyOfMethodArgumentsUsed
in class AbstractOperationPO
true
use copy of method call arguments,
false
use original method call arguments.protected java.lang.String buildPOName(boolean transactionFlag)
Proof
based on the given transaction flag.buildPOName
in class AbstractOperationPO
transactionFlag
- The transaction flag.public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public java.lang.String getPrecondition()
public void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
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).fillSaveProperties
in interface IPersistablePO
fillSaveProperties
in class AbstractOperationPO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public static java.lang.String getProgramMethodSignature(IProgramMethod pm, boolean includeType) throws java.io.IOException
pm
- The IProgramMethod
which provides the signature.includeType
- Include the container type?java.io.IOException
- Occurred Exception.public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, java.util.Properties properties) throws java.io.IOException
initConfig
- The already load InitConfig
.properties
- The settings of the proof obligation to instantiate.java.io.IOException
- Occurred Exception.public static IProgramMethod getProgramMethod(InitConfig initConfig, java.util.Properties properties) throws java.io.IOException
IProgramMethod
defined by the given Properties
.initConfig
- The already load InitConfig
.properties
- The settings of the proof obligation to instantiate.IProgramMethod
.java.io.IOException
- Occurred Exception if it was not possible to find the IProgramMethod
.public static java.lang.String getPrecondition(java.util.Properties properties)
properties
- The proof obligation settings to read from.null
if not available.protected Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in class AbstractOperationPO
public KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.getContainerType
in interface ProofOblInput
getContainerType
in class AbstractPO
KeYJavaType
in which the proven element is contained in or null
if not available.