de.uka.ilkd.key.proof.init

Class FunctionalLoopContractPO

java.lang.Object

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

de.uka.ilkd.key.proof.init.FunctionalLoopContractPO

All Implemented Interfaces:

ContractPO, IPersistablePO, ProofOblInput

public class FunctionalLoopContractPO
extends AbstractPO
implements ContractPO

A proof obligation for a FunctionalLoopContract.

Author:

lanzinger

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.proof.init.AbstractPO

AbstractPO.Vertex

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 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.

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
FunctionalLoopContractPO(InitConfig initConfig, FunctionalLoopContract contract)

Method Summary

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)

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

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

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.proof.init.ProofOblInput

getContainerType, getPO, name

Field Detail

TRANSACTION_TAGS

private static final java.util.Map<java.lang.Boolean,java.lang.String> TRANSACTION_TAGS

Transaction tags.

contract

private FunctionalLoopContract contract

The contract from which this PO is generated.

proofConfig

private InitConfig proofConfig

The initial proof configuration.

Constructor Detail

FunctionalLoopContractPO

public FunctionalLoopContractPO(InitConfig initConfig,
                                FunctionalLoopContract contract)

Parameters:

initConfig - the initial proof configuration.

contract - the contract from which this PO is generated.

Method Detail

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.

fillSaveProperties

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

Description copied from class: AbstractPO

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 AbstractPO

Parameters:

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

Throws:

java.io.IOException - Occurred Exception.

implies

public boolean implies(ProofOblInput po)

Description copied from interface: ProofOblInput

If true, then this PO implies the passed one.

Specified by:

implies in interface ProofOblInput

Overrides:

implies in class AbstractPO

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

readProblem

public void readProblem()
                 throws ProofInputException

Specified by:

readProblem in interface ProofOblInput

Throws:

ProofInputException

getBlock

public StatementBlock getBlock()

Returns:

the contract's block.

See Also:

AuxiliaryContract.getBlock()

getCalleeKeYJavaType

public KeYJavaType getCalleeKeYJavaType()

Returns:

the type containing this contract.

See Also:

SpecificationElement.getKJT()

getProgramMethod

public IProgramMethod getProgramMethod()

Returns:

the method containing this contract.

See Also:

AuxiliaryContract.getMethod()

getContract

public Contract getContract()

Specified by:

getContract in interface ContractPO

getMbyAtPre

public Term getMbyAtPre()

Specified by:

getMbyAtPre in interface ContractPO

postInit

protected Services postInit()

Initializes the proof configuration.

Returns:

the services from the proof configuration.

getCreatedInitConfigForSingleProof

protected InitConfig getCreatedInitConfigForSingleProof()

Specified by:

getCreatedInitConfigForSingleProof in class AbstractPO

createPostconditions

private Term[] createPostconditions(java.util.Map<LocationVariable,Term> modifiesClauses,
                                    AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)

Parameters:

modifiesClauses - the contract's modifies clauses.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder

Returns:

the contract's postconditions.

createPostconditionsNext

private Term[] createPostconditionsNext(Term selfTerm,
                                        java.util.List<LocationVariable> heaps,
                                        AuxiliaryContract.Variables nextVariables,
                                        java.util.Map<LocationVariable,Term> modifiesClauses,
                                        Services services)

createAssumptions

private Term[] createAssumptions(ProgramVariable selfVar,
                                 java.util.List<LocationVariable> heaps,
                                 Term wellFormedHeapsCondition,
                                 Services services,
                                 AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)

Parameters:

selfVar - the self variable.

heaps - the heaps.

wellFormedHeapsCondition - the condition that all heaps are well-formed.

services - services.

conditionsAndClausesBuilder - a conditions and clauses builder.

Returns:

the preconditions.

createAnonInHeaps

private static java.util.Map<LocationVariable,Function> createAnonInHeaps(java.util.List<LocationVariable> heaps,
                                                                          Services services,
                                                                          TermBuilder tb)

Parameters:

heaps - heaps.

services - services.

tb - a term builder.

Returns:

a map from every heap to an anonymization heap.

createAnonOutHeaps

private java.util.Map<LocationVariable,Function> createAnonOutHeaps(java.util.List<LocationVariable> heaps,
                                                                    Services services,
                                                                    TermBuilder tb)

Parameters:

heaps - heaps.

services - services.

tb - a term builder.

Returns:

a map from every heap to an anonymization heap.

createGoalConfigurator

private AuxiliaryContractBuilders.GoalsConfigurator createGoalConfigurator(ProgramVariable selfVar,
                                                                           Term selfTerm,
                                                                           AuxiliaryContract.Variables variables,
                                                                           Services services,
                                                                           TermBuilder tb)

Parameters:

selfVar - the self variable.

selfTerm - the self term.

variables - the contract's variables.

services - services.

tb - a term builder.

Returns:

a goal configurator.

setUpValidityGoal

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)

Parameters:

selfTerm - the self term

heaps - 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.

Returns:

the validity formula for the contract.