de.uka.ilkd.key.proof.init

Class DependencyContractPO

java.lang.Object

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

de.uka.ilkd.key.proof.init.DependencyContractPO

All Implemented Interfaces:

ContractPO, IPersistablePO, ProofOblInput

public final class DependencyContractPO
extends AbstractPO
implements ContractPO

The proof obligation for dependency contracts.

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 DependencyContract	contract
private Term	mbyAtPre
private InitConfig	proofConfig
private TermBuilder	tb

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

environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets

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
DependencyContractPO(InitConfig initConfig, DependencyContract contract)

Method Summary

Modifier and Type	Method and Description
private Term	buildFreePre(java.util.List<LocationVariable> heaps, ProgramVariable selfVar, KeYJavaType selfKJT, ImmutableList<ProgramVariable> paramVars, Term wellFormedHeaps, Services services)
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.
KeYJavaType	getContainerType() Returns the KeYJavaType in which the proven element is contained in.
DependencyContract	getContract()
protected InitConfig	getCreatedInitConfigForSingleProof()
Term	getMbyAtPre()
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.
private Services	postInit()
void	readProblem()

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

assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, generateWdTaclets, 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

getPO, name

Field Detail

mbyAtPre

private Term mbyAtPre

contract

private DependencyContract contract

proofConfig

private InitConfig proofConfig

tb

private TermBuilder tb

Constructor Detail

DependencyContractPO

public DependencyContractPO(InitConfig initConfig,
                            DependencyContract contract)

Method Detail

buildFreePre

private Term buildFreePre(java.util.List<LocationVariable> heaps,
                          ProgramVariable selfVar,
                          KeYJavaType selfKJT,
                          ImmutableList<ProgramVariable> paramVars,
                          Term wellFormedHeaps,
                          Services services)
                   throws ProofInputException

Throws:

ProofInputException

readProblem

public void readProblem()
                 throws ProofInputException

Specified by:

readProblem in interface ProofOblInput

Throws:

ProofInputException

postInit

private Services postInit()

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

getContract

public DependencyContract getContract()

Specified by:

getContract in interface ContractPO

getMbyAtPre

public Term getMbyAtPre()

Specified by:

getMbyAtPre in interface ContractPO

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

fillSaveProperties

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

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.

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.

getCreatedInitConfigForSingleProof

protected InitConfig getCreatedInitConfigForSingleProof()

Specified by:

getCreatedInitConfigForSingleProof in class AbstractPO

getContainerType

public KeYJavaType getContainerType()

Returns the KeYJavaType in which the proven element is contained in.

Specified by:

getContainerType in interface ProofOblInput

Overrides:

getContainerType in class AbstractPO

Returns:

The KeYJavaType in which the proven element is contained in or null if not available.