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.
ProofSaver
,
ProblemLoader
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. |
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() . |
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 . |
getContainerType, getPO, implies, name, readProblem
static final java.lang.String PROPERTY_CLASS
#getClass()
.static final java.lang.String PROPERTY_NAME
ProofOblInput.name()
.static final java.lang.String PROPERTY_FILENAME
static final java.lang.String PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL
AbstractOperationPO.isAddSymbolicExecutionLabel()
.static final java.lang.String PROPERTY_ADD_UNINTERPRETED_PREDICATE
AbstractOperationPO.isAddUninterpretedPredicate()
.void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
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).properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.