de.uka.ilkd.key.proof.init

Interface IPersistablePO

All Superinterfaces:

ProofOblInput

All Known Implementing Classes:

AbstractInfFlowPO, AbstractOperationPO, AbstractPO, BlockExecutionPO, DependencyContractPO, FunctionalBlockContractPO, FunctionalLoopContractPO, FunctionalOperationContractPO, InfFlowContractPO, LoopInvExecutionPO, ProgramMethodPO, ProgramMethodSubsetPO, SymbolicExecutionPO, TacletProofObligationInput, WellDefinednessPO

public interface IPersistablePO
extends ProofOblInput

This interface extends the standard proof obligation (ProofOblInput) with functionality to define the individual parameters which are required for loading and saving *.proof files.

During save process the ProofSaver calls method fillSaveProperties(Properties). This proof obligation has to store all information in the given Properties which are required to reconstruct it. The class (#getClass()) of this class must be stored in the Properties with key PROPERTY_CLASS.

During load process the ProblemLoader tries to execute a static method on the class defined via Properties key PROPERTY_CLASS with the following signature: public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) throws IOException The returned IPersistablePO.LoadedPOContainer contains the instantiated ProofOblInput together with the proof index.

Author:

Martin Hentschel

See Also:

ProofSaver, ProblemLoader

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	IPersistablePO.LoadedPOContainer The class stored in a Properties instance via key must provide the static method with the following signature: public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) throws IOException This method is called by the ProblemLoader to recreate a proof obligation.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL The key used to store AbstractOperationPO.isAddSymbolicExecutionLabel().
static java.lang.String	PROPERTY_ADD_UNINTERPRETED_PREDICATE The key used to store AbstractOperationPO.isAddUninterpretedPredicate().
static java.lang.String	PROPERTY_CLASS The key used to store #getClass().
static java.lang.String	PROPERTY_FILENAME The key used to store the file name under which a PO is loaded.
static java.lang.String	PROPERTY_NAME The key used to store ProofOblInput.name().

Method Summary

Modifier and Type	Method and Description
void	fillSaveProperties(java.util.Properties properties) This method is called by a ProofSaver to store the proof specific settings in the given Properties.

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

getContainerType, getPO, implies, name, readProblem

Field Detail

PROPERTY_CLASS

static final java.lang.String PROPERTY_CLASS

The key used to store #getClass().

See Also:

Constant Field Values

PROPERTY_NAME

static final java.lang.String PROPERTY_NAME

The key used to store ProofOblInput.name().

See Also:

Constant Field Values

PROPERTY_FILENAME

static final java.lang.String PROPERTY_FILENAME

The key used to store the file name under which a PO is loaded. This key is set during loading by the loader and needs not be saved.

See Also:

Constant Field Values

PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL

static final java.lang.String PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL

The key used to store AbstractOperationPO.isAddSymbolicExecutionLabel().

See Also:

Constant Field Values

PROPERTY_ADD_UNINTERPRETED_PREDICATE

static final java.lang.String PROPERTY_ADD_UNINTERPRETED_PREDICATE

The key used to store AbstractOperationPO.isAddUninterpretedPredicate().

See Also:

Constant Field Values

Method Detail

fillSaveProperties

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

Parameters:

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

Throws:

java.io.IOException - Occurred Exception.