public class TacletProofObligationInput extends java.lang.Object implements ProofOblInput, IPersistablePO
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private java.lang.String[] |
axiomFiles |
private java.lang.String |
baseDir |
private java.lang.String |
definitionFile |
private InitConfig |
environmentConfig |
private TacletSoundnessPOLoader.TacletFilter |
filter
This filter is used to filter out precisely that taclet which has the
required name.
|
private TacletSoundnessPOLoader.LoaderListener |
listener
This listener communicates with the PO loader.
|
private ProofAggregate |
proofObligation |
private java.lang.String |
tacletFile |
private java.lang.String |
tacletName |
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
TacletProofObligationInput(java.lang.String tacletName,
InitConfig initConfig)
Instantiates a new taclet proof obligation input object.
|
Modifier and Type | Method and Description |
---|---|
private ProofEnvironment |
createProofEnvironment() |
private java.util.Collection<java.io.File> |
fileCollection(java.lang.String[] strings) |
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. |
ProofAggregate |
getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
static IPersistablePO.LoadedPOContainer |
loadFrom(InitConfig initConfig,
java.util.Properties properties) |
java.lang.String |
name()
Returns the name of the proof obligation input.
|
void |
readProblem() |
void |
setLoadInfo(java.io.File tacletFile,
java.io.File definitionFile,
java.util.Collection<java.io.File> axiomFiles) |
private void |
setLoadInfo(java.util.Properties properties) |
private java.lang.String tacletName
private ProofAggregate proofObligation
private java.lang.String definitionFile
private java.lang.String tacletFile
private java.lang.String[] axiomFiles
private java.lang.String baseDir
private TacletSoundnessPOLoader.TacletFilter filter
private TacletSoundnessPOLoader.LoaderListener listener
private final InitConfig environmentConfig
public TacletProofObligationInput(java.lang.String tacletName, InitConfig initConfig)
tacletName
- the name of the taclet which is to be createdinitConfig
- the initconfig under which the PO is to be examinedpublic void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
IPersistablePO
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
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public java.lang.String name()
ProofOblInput
name
in interface ProofOblInput
public void readProblem() throws ProofInputException
readProblem
in interface ProofOblInput
ProofInputException
private ProofEnvironment createProofEnvironment() throws ProofInputException
ProofInputException
private java.util.Collection<java.io.File> fileCollection(java.lang.String[] strings)
public ProofAggregate getPO() throws ProofInputException
ProofOblInput
getPO
in interface ProofOblInput
ProofInputException
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, java.util.Properties properties)
private void setLoadInfo(java.util.Properties properties)
public void setLoadInfo(java.io.File tacletFile, java.io.File definitionFile, java.util.Collection<java.io.File> axiomFiles)
public KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.getContainerType
in interface ProofOblInput
KeYJavaType
in which the proven element is contained in or null
if not available.