public class FunctionalBlockContractPO extends AbstractPO implements ContractPO
FunctionalBlockContract
.AbstractPO.Vertex
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private FunctionalBlockContract |
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 |
---|
FunctionalBlockContractPO(InitConfig initConfig,
FunctionalBlockContract contract) |
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 FunctionalBlockContract contract
private InitConfig proofConfig
public FunctionalBlockContractPO(InitConfig initConfig, FunctionalBlockContract 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.private static Term createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOutVariables, Services services, TermBuilder tb)
localOuts
- a set of variables.services
- services.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 static java.util.Map<LocationVariable,Function> createAnonOutHeaps(java.util.List<LocationVariable> heaps, FunctionalBlockContract contract, Services services, TermBuilder tb)
heaps
- heaps.services
- services.tb
- a term builder.private static Term[] createUpdates(AuxiliaryContract.Variables variables, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonHeaps, Services services)
variables
- the contract's variables.heaps
- the heaps.anonHeaps
- the anonymization heaps.services
- services.private static Term[] createPostconditions(AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
conditionsAndClausesBuilder
- a conditions and clauses builder.private static Term setUpValidityTerm(java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonHeaps, java.util.Map<LocationVariable,Function> anonOutHeaps, ImmutableSet<ProgramVariable> localInVariables, ImmutableSet<ProgramVariable> localOutVariables, ProgramVariable exceptionParameter, Term[] assumptions, Term[] postconditions, Term[] updates, BlockContract bc, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services, TermBuilder tb)
heaps
- the heaps.anonHeaps
- the heaps used in the anonIn update.anonOutHeaps
- the heaps used in the anonOut update.localInVariables
- the free local variables in the block.localOutVariables
- the free local variables modified by the block.exceptionParameter
- the exception variable.assumptions
- the preconditions.postconditions
- the postconditions.updates
- the update.bc
- the contract being applied.conditionsAndClausesBuilder
- a conditions and clauses builder.configurator
- a goal configurator.services
- services.tb
- a term builder.private static Term addWdToValidityTerm(Term validity, Term[] updates, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonOutHeaps, ImmutableSet<ProgramVariable> localInVariables, ImmutableSet<ProgramVariable> localOutVariables, BlockContract bc, AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services, TermBuilder tb)
validity
- the validity formula.updates
- the updates.heaps
- the heaps.anonOutHeaps
- the heaps used in the anonOut update.localInVariables
- the free local variables in the block.localOutVariables
- the free local variables modified by the block.bc
- the contract being applied.configurator
- a goal configuratorservices
- services.tb
- a term builder.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 AuxiliaryContractBuilders.GoalsConfigurator setUpGoalConfigurator(StatementBlock block, ProgramVariable selfVar, Term selfTerm, AuxiliaryContract.Variables variables, Services services, TermBuilder tb)
block
- the block this contract belongs to.selfVar
- the self variable.selfTerm
- the self term.variables
- the contract's variables.services
- services.tb
- a term builder.private Term[] createAssumptions(IProgramMethod pm, ProgramVariable selfVar, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services)
pm
- the method this contract belongs to.selfVar
- the self variable.heaps
- the heaps.localInVariables
- the free local variables in the block.conditionsAndClausesBuilder
- a conditions and clauses builder.services
- services.