public class FunctionalOperationContractPO extends AbstractOperationPO implements ContractPO
The proof obligation for operation contracts.
The generated Sequent
has the following form:
==>
<generalAssumptions> &
<preconditions>
->
<updatesToStoreInitialValues>
<modalityStart>
exc=null;try {<methodBodyExpand>}catch(java.lang.Throwable e) {exc = e}
<modalityEnd>
(exc = null & <postconditions > & <optionalUninterpretedPredicate>)
AbstractPO.Vertex
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private FunctionalOperationContract |
contract |
protected Term |
mbyAtPre |
static java.util.Map<java.lang.Boolean,java.lang.String> |
TRANSACTION_TAGS |
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 |
---|
FunctionalOperationContractPO(InitConfig initConfig,
FunctionalOperationContract contract)
Constructor.
|
FunctionalOperationContractPO(InitConfig initConfig,
FunctionalOperationContract contract,
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. |
protected Term |
buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
boolean |
equals(java.lang.Object o) |
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. |
FunctionalOperationContract |
getContract() |
protected Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
getMbyAtPre() |
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.
|
protected IProgramMethod |
getProgramMethod()
Returns the
IProgramMethod to call. |
protected Modality |
getTerminationMarker()
Returns the
Modality to use as termination marker. |
int |
hashCode() |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
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, createUninterpretedPredicate, ensureUninterpretedPredicateExists, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit, readProblem
assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, generateWdTaclets, getName, getPO, name, register, register, register, selectClassAxioms
clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait
getPO, name, readProblem
public static java.util.Map<java.lang.Boolean,java.lang.String> TRANSACTION_TAGS
private FunctionalOperationContract contract
protected Term mbyAtPre
public FunctionalOperationContractPO(InitConfig initConfig, FunctionalOperationContract contract)
initConfig
- The InitConfig
to use.contract
- The FunctionalOperationContractPO
to prove.public FunctionalOperationContractPO(InitConfig initConfig, FunctionalOperationContract contract, boolean addUninterpretedPredicate, boolean addSymbolicExecutionLabel)
initConfig
- The InitConfig
to use.contract
- The FunctionalOperationContractPO
to prove.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.protected 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 getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in class AbstractOperationPO
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 Term buildUpdate(ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
buildUpdate
in class AbstractOperationPO
paramVars
- Formal parameters of method call.formalParamVars
- Arguments from formal parameters for method call.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The services instance.Term
representing the initial updates.protected java.lang.String buildPOName(boolean transactionFlag)
Proof
based on the given transaction flag.buildPOName
in class AbstractOperationPO
transactionFlag
- The transaction flag.public FunctionalOperationContract getContract()
getContract
in interface ContractPO
public Term getMbyAtPre()
getMbyAtPre
in interface ContractPO
public boolean implies(ProofOblInput po)
implies
in interface ProofOblInput
implies
in class AbstractPO
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
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 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 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.