public abstract class AbstractPO extends java.lang.Object implements IPersistablePO
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
protected InitConfig |
environmentConfig |
protected Services |
environmentServices |
protected HeapLDT |
heapLDT |
protected JavaInfo |
javaInfo |
protected java.lang.String |
name |
protected java.lang.String[] |
poNames |
protected Term[] |
poTerms |
protected SpecificationRepository |
specRepos |
protected ImmutableSet<NoPosTacletApp> |
taclets |
protected TermBuilder |
tb |
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
AbstractPO(InitConfig initConfig,
java.lang.String name) |
Modifier and Type | Method and Description |
---|---|
protected void |
assignPOTerms(Term... poTerms) |
protected void |
collectClassAxioms(KeYJavaType selfKJT,
InitConfig proofConfig) |
protected Proof |
createProof(java.lang.String proofName,
Term poTerm,
InitConfig proofConfig)
Creates a Proof (helper for getPO()).
|
protected Proof |
createProofObject(java.lang.String proofName,
java.lang.String proofHeader,
Term poTerm,
InitConfig proofConfig) |
void |
fillSaveProperties(java.util.Properties properties)
This method is called by a
ProofSaver to store the proof
specific settings in the given Properties . |
protected Term |
generateSelfCreated(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
ProgramVariable selfVar,
Services services)
Generates the general assumption that self is created.
|
protected Term |
generateSelfExactType(IProgramMethod pm,
ProgramVariable selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected Term |
generateSelfExactType(IProgramMethod pm,
Term selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected Term |
generateSelfNotNull(IProgramMethod pm,
ProgramVariable selfVar)
Generates the general assumption that self is not null.
|
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
protected abstract InitConfig |
getCreatedInitConfigForSingleProof() |
static java.lang.String |
getName(java.util.Properties properties)
Returns the name value from the given properties.
|
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.
|
java.lang.String |
name()
Returns the name of the proof obligation input.
|
protected void |
register(Function f,
Services services) |
protected void |
register(ImmutableList<ProgramVariable> pvs,
Services services) |
protected void |
register(ProgramVariable pv,
Services services) |
protected ImmutableSet<ClassAxiom> |
selectClassAxioms(KeYJavaType selfKJT) |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
readProblem
protected TermBuilder tb
protected final InitConfig environmentConfig
protected Services environmentServices
protected final JavaInfo javaInfo
protected final HeapLDT heapLDT
protected final SpecificationRepository specRepos
protected final java.lang.String name
protected ImmutableSet<NoPosTacletApp> taclets
protected Term[] poTerms
protected java.lang.String[] poNames
public AbstractPO(InitConfig initConfig, java.lang.String name)
protected ImmutableSet<ClassAxiom> selectClassAxioms(KeYJavaType selfKJT)
protected void collectClassAxioms(KeYJavaType selfKJT, InitConfig proofConfig)
protected final void register(ProgramVariable pv, Services services)
protected final void register(ImmutableList<ProgramVariable> pvs, Services services)
protected Term generateSelfNotNull(IProgramMethod pm, ProgramVariable selfVar)
pm
- The IProgramMethod
to execute.selfVar
- The self variable.protected Term generateSelfCreated(java.util.List<LocationVariable> heaps, IProgramMethod pm, ProgramVariable selfVar, Services services)
heaps
- The heap contextpm
- The IProgramMethod
to execute.selfVar
- The self variable.services
- The services instance.protected Term generateSelfExactType(IProgramMethod pm, ProgramVariable selfVar, KeYJavaType selfKJT)
pm
- The IProgramMethod
to execute.selfVar
- The self variable.selfKJT
- The KeYJavaType
of the self variable.protected Term generateSelfExactType(IProgramMethod pm, Term selfVar, KeYJavaType selfKJT)
pm
- The IProgramMethod
to execute.selfVar
- The self variable.selfKJT
- The KeYJavaType
of the self variable.public final java.lang.String name()
ProofOblInput
name
in interface ProofOblInput
protected Proof createProof(java.lang.String proofName, Term poTerm, InitConfig proofConfig)
proofName
- name of the proofpoTerm
- term of the proof obligationproofConfig
- the proof configurationprotected Proof createProofObject(java.lang.String proofName, java.lang.String proofHeader, Term poTerm, InitConfig proofConfig)
protected abstract InitConfig getCreatedInitConfigForSingleProof()
public final ProofAggregate getPO()
ProofOblInput
getPO
in interface ProofOblInput
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
protected void assignPOTerms(Term... poTerms)
public 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).fillSaveProperties
in interface IPersistablePO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public static java.lang.String getName(java.util.Properties properties)
properties
- The properties to read from.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.Copyright © 2003-2019 The KeY-Project.