public abstract class AbstractPO extends java.lang.Object implements IPersistablePO
Modifier and Type | Class and Description |
---|---|
(package private) static class |
AbstractPO.Vertex
Represents a vertex and additional information required by the Tarjan algorithm.
|
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private java.util.HashMap<AbstractPO.Vertex,ImmutableList<Pair<Sort,IObserverFunction>>> |
allSCCs |
protected InitConfig |
environmentConfig |
protected Services |
environmentServices |
private java.lang.String |
header |
protected HeapLDT |
heapLDT |
private int |
index
number of currently visited nodes
|
protected JavaInfo |
javaInfo |
protected java.lang.String |
name |
protected java.lang.String[] |
poNames |
protected Term[] |
poTerms |
private ProofAggregate |
proofAggregate |
protected SpecificationRepository |
specRepos |
private java.util.ArrayDeque<AbstractPO.Vertex> |
stack |
protected ImmutableSet<NoPosTacletApp> |
taclets |
protected TermBuilder |
tb |
private java.util.HashMap<Pair<Sort,IObserverFunction>,AbstractPO.Vertex> |
vertices |
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) |
private boolean |
choicesApply(Taclet taclet,
ImmutableSet<Choice> choices)
Check whether a taclet conforms with the currently active choices.
|
protected void |
collectClassAxioms(KeYJavaType selfKJT,
InitConfig proofConfig) |
protected Proof |
createProof(java.lang.String proofName,
Term poTerm,
InitConfig proofConfig)
Creates a Proof (helper for getPO()).
|
private void |
createProofHeader(java.lang.String javaPath,
java.lang.String classPath,
java.lang.String bootClassPath,
java.lang.String includedFiles,
Services services)
Creates declarations necessary to save/load proof in textual form
(helper for createProof()).
|
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.
|
(package private) void |
generateWdTaclets(InitConfig proofConfig)
Generate well-definedness taclets to resolve formulas as
WD(pv.
|
private ImmutableSet<ClassAxiom> |
getAxiomsForObserver(Pair<Sort,IObserverFunction> usedObs,
ImmutableSet<ClassAxiom> axioms) |
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.
|
private void |
getSCCForNode(AbstractPO.Vertex node,
ImmutableSet<ClassAxiom> axioms,
InitConfig proofConfig)
computes all strongly connected components reachable by the given node and adds them
to
allSCCs |
private AbstractPO.Vertex |
getVertexFor(Pair<Sort,IObserverFunction> vertexCore,
ClassAxiom axiom) |
private AbstractPO.Vertex |
getVertexFor(Sort targetSort,
IObserverFunction observer,
ClassAxiom axiom) |
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) |
private void |
register(Taclet t,
InitConfig proofConfig) |
private void |
registerClassAxiomTaclets(KeYJavaType selfKJT,
InitConfig proofConfig)
adds all taclets for the class axioms accessible and needed by this PO
|
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
private java.lang.String header
private ProofAggregate proofAggregate
private java.util.HashMap<AbstractPO.Vertex,ImmutableList<Pair<Sort,IObserverFunction>>> allSCCs
private final java.util.HashMap<Pair<Sort,IObserverFunction>,AbstractPO.Vertex> vertices
private final java.util.ArrayDeque<AbstractPO.Vertex> stack
private int index
public AbstractPO(InitConfig initConfig, java.lang.String name)
private ImmutableSet<ClassAxiom> getAxiomsForObserver(Pair<Sort,IObserverFunction> usedObs, ImmutableSet<ClassAxiom> axioms)
void generateWdTaclets(InitConfig proofConfig)
proofConfig
- the proof configurationprotected ImmutableSet<ClassAxiom> selectClassAxioms(KeYJavaType selfKJT)
protected void collectClassAxioms(KeYJavaType selfKJT, InitConfig proofConfig)
private boolean choicesApply(Taclet taclet, ImmutableSet<Choice> choices)
choices
.private void register(Taclet t, 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.private AbstractPO.Vertex getVertexFor(Sort targetSort, IObserverFunction observer, ClassAxiom axiom)
private AbstractPO.Vertex getVertexFor(Pair<Sort,IObserverFunction> vertexCore, ClassAxiom axiom)
private void registerClassAxiomTaclets(KeYJavaType selfKJT, InitConfig proofConfig)
selfKJT
- the KeYJavaType
for which to collect all accessible class axiomsproofConfig
- the InitConfig
of the proof for this POprivate void getSCCForNode(AbstractPO.Vertex node, ImmutableSet<ClassAxiom> axioms, InitConfig proofConfig)
allSCCs
node
- the starting AbstractPO.Vertex
axioms
- set of ClassAxiom
used to compute the outgoing edges of the nodesproofConfig
- the InitConfig
of the proof for this POpublic final java.lang.String name()
ProofOblInput
name
in interface ProofOblInput
private void createProofHeader(java.lang.String javaPath, java.lang.String classPath, java.lang.String bootClassPath, java.lang.String includedFiles, Services services)
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.