public class FunctionalLoopContractPO extends AbstractPO implements ContractPO
FunctionalLoopContract
.AbstractPO.Vertex
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private FunctionalLoopContract |
contract
The contract from which this PO is generated.
|
private InitConfig |
proofConfig
The initial proof configuration.
|
private static java.util.Map<java.lang.Boolean,java.lang.String> |
TRANSACTION_TAGS
Transaction tags.
|
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 |
---|
FunctionalLoopContractPO(InitConfig initConfig,
FunctionalLoopContract contract) |
Modifier and Type | Method and Description |
---|---|
private static java.util.Map<LocationVariable,Function> |
createAnonInHeaps(java.util.List<LocationVariable> heaps,
Services services,
TermBuilder tb) |
private java.util.Map<LocationVariable,Function> |
createAnonOutHeaps(java.util.List<LocationVariable> heaps,
Services services,
TermBuilder tb) |
private Term[] |
createAssumptions(ProgramVariable selfVar,
java.util.List<LocationVariable> heaps,
Term wellFormedHeapsCondition,
Services services,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder) |
private AuxiliaryContractBuilders.GoalsConfigurator |
createGoalConfigurator(ProgramVariable selfVar,
Term selfTerm,
AuxiliaryContract.Variables variables,
Services services,
TermBuilder tb) |
private Term[] |
createPostconditions(java.util.Map<LocationVariable,Term> modifiesClauses,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder) |
private Term[] |
createPostconditionsNext(Term selfTerm,
java.util.List<LocationVariable> heaps,
AuxiliaryContract.Variables nextVariables,
java.util.Map<LocationVariable,Term> modifiesClauses,
Services services) |
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 . |
StatementBlock |
getBlock() |
KeYJavaType |
getCalleeKeYJavaType() |
Contract |
getContract() |
protected InitConfig |
getCreatedInitConfigForSingleProof() |
Term |
getMbyAtPre() |
IProgramMethod |
getProgramMethod() |
int |
hashCode() |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
static IPersistablePO.LoadedPOContainer |
loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
protected Services |
postInit()
Initializes the proof configuration.
|
void |
readProblem() |
private Term |
setUpValidityGoal(Term selfTerm,
java.util.List<LocationVariable> heaps,
java.util.Map<LocationVariable,Function> anonOutHeaps,
AuxiliaryContract.Variables variables,
AuxiliaryContract.Variables nextVariables,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
Term wellFormedHeapsCondition,
AuxiliaryContractBuilders.GoalsConfigurator configurator,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
Services services,
TermBuilder tb) |
assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, generateWdTaclets, getContainerType, getName, getPO, name, register, register, register, selectClassAxioms
clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait
getContainerType, getPO, name
private static final java.util.Map<java.lang.Boolean,java.lang.String> TRANSACTION_TAGS
private FunctionalLoopContract contract
private InitConfig proofConfig
public FunctionalLoopContractPO(InitConfig initConfig, FunctionalLoopContract contract)
initConfig
- the initial proof configuration.contract
- the contract from which this PO is generated.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 void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
AbstractPO
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 AbstractPO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
implies
in class AbstractPO
public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public void readProblem() throws ProofInputException
readProblem
in interface ProofOblInput
ProofInputException
public StatementBlock getBlock()
AuxiliaryContract.getBlock()
public KeYJavaType getCalleeKeYJavaType()
SpecificationElement.getKJT()
public IProgramMethod getProgramMethod()
AuxiliaryContract.getMethod()
public Contract getContract()
getContract
in interface ContractPO
public Term getMbyAtPre()
getMbyAtPre
in interface ContractPO
protected Services postInit()
protected InitConfig getCreatedInitConfigForSingleProof()
getCreatedInitConfigForSingleProof
in class AbstractPO
private Term[] createPostconditions(java.util.Map<LocationVariable,Term> modifiesClauses, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
modifiesClauses
- the contract's modifies clauses.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilderprivate Term[] createPostconditionsNext(Term selfTerm, java.util.List<LocationVariable> heaps, AuxiliaryContract.Variables nextVariables, java.util.Map<LocationVariable,Term> modifiesClauses, Services services)
private Term[] createAssumptions(ProgramVariable selfVar, java.util.List<LocationVariable> heaps, Term wellFormedHeapsCondition, Services services, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
selfVar
- the self variable.heaps
- the heaps.wellFormedHeapsCondition
- the condition that all heaps are well-formed.services
- services.conditionsAndClausesBuilder
- a conditions and clauses builder.private static java.util.Map<LocationVariable,Function> createAnonInHeaps(java.util.List<LocationVariable> heaps, Services services, TermBuilder tb)
heaps
- heaps.services
- services.tb
- a term builder.private java.util.Map<LocationVariable,Function> createAnonOutHeaps(java.util.List<LocationVariable> heaps, Services services, TermBuilder tb)
heaps
- heaps.services
- services.tb
- a term builder.private AuxiliaryContractBuilders.GoalsConfigurator createGoalConfigurator(ProgramVariable selfVar, Term selfTerm, AuxiliaryContract.Variables variables, Services services, TermBuilder tb)
selfVar
- the self variable.selfTerm
- the self term.variables
- the contract's variables.services
- services.tb
- a term builder.private Term setUpValidityGoal(Term selfTerm, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonOutHeaps, AuxiliaryContract.Variables variables, AuxiliaryContract.Variables nextVariables, java.util.Map<LocationVariable,Term> modifiesClauses, Term[] assumptions, Term decreasesCheck, Term[] postconditions, Term[] postconditionsNext, Term wellFormedHeapsCondition, AuxiliaryContractBuilders.GoalsConfigurator configurator, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services, TermBuilder tb)
selfTerm
- the self termheaps
- the heaps.anonOutHeaps
- the heaps used in the anonOut update.variables
- the contract's variables.nextVariables
- the variables for the next loop iteration.modifiesClauses
- the modified clauses.assumptions
- the preconditions.decreasesCheck
- the decreases check.postconditions
- the postconditions for the current loop iteration.postconditionsNext
- the postconditions for the next loop iteration.wellFormedHeapsCondition
- the condition that all heaps are well-formed.configurator
- a goal configurator.conditionsAndClausesBuilder
- a conditions and clauses builder.services
- services.tb
- a term builder.