public class InfFlowProof extends Proof
Modifier and Type | Field and Description |
---|---|
private InfFlowProofSymbols |
infFlowSymbols
For saving and loading Information-Flow proofs, we need to remember the
according taclets, program variables, functions and such.
|
private SideProofStatistics |
sideProofStatistics
Aggregated proof statistics from other proofs which contributed to this one.
|
keyVersionLog, userLog
Constructor and Description |
---|
InfFlowProof(java.lang.String name,
InitConfig initConfig) |
InfFlowProof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
InfFlowProof(java.lang.String name,
Term problem,
java.lang.String header,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
void |
addGoalTemplates(Taclet t) |
void |
addIFSymbol(java.lang.Object s) |
void |
addLabeledIFSymbol(java.lang.Object s) |
void |
addLabeledTotalTerm(Term p) |
void |
addSideProof(InfFlowProof proof) |
private void |
addSideProofStatistics(Statistics stat) |
void |
addTotalTerm(Term p) |
InfFlowProofSymbols |
getIFSymbols() |
SideProofStatistics |
getSideProofStatistics()
returns statistics of possible side proofs that contributed to this proof
|
boolean |
hasSideProofs() |
java.lang.String |
printIFSymbols() |
InfFlowProofSymbols |
removeInfFlowProofSymbols() |
void |
unionIFSymbols(InfFlowProofSymbols symbols) |
void |
unionLabeledIFSymbols(InfFlowProofSymbols symbols) |
abbreviations, add, add, addAutoModeTime, addProofDisposedListener, addProofTreeListener, addRuleAppListener, breadthFirstSearch, clearAndDetachRuleAppIndexes, closed, closeGoal, containsProofTreeListener, countBranches, countNodes, dispose, find, fireNotesChanged, fireProofClosed, fireProofDisposed, fireProofDisposing, fireProofExpanded, fireProofGoalRemoved, fireProofGoalsAdded, fireProofGoalsAdded, fireProofGoalsChanged, fireProofIsBeingPruned, fireProofPruned, fireProofStructureChanged, fireRuleApplied, getActiveStrategy, getActiveStrategyFactory, getAutoModeTime, getClosedGoal, getClosedSubtreeGoals, getEnv, getGoal, getInitConfig, getJavaInfo, getNamespaces, getProofDisposedListeners, getProofFile, getProofIndependentSettings, getServices, getSettings, getStatistics, getSubtreeEnabledGoals, getSubtreeGoals, header, isClosedGoal, isDisposed, isGoal, mgt, name, openEnabledGoals, openGoals, pruneProof, pruneProof, pruneProof, removeProofDisposedListener, removeProofTreeListener, removeRuleAppListener, reOpenGoal, replace, root, saveToFile, setActiveStrategy, setEnv, setNamespaces, setProofFile, setRoot, setRuleAppIndexToAutoMode, setRuleAppIndexToInteractiveMode, toString, traverseFromChildToParent
private InfFlowProofSymbols infFlowSymbols
private SideProofStatistics sideProofStatistics
public InfFlowProof(java.lang.String name, Sequent sequent, java.lang.String header, TacletIndex rules, BuiltInRuleIndex builtInRules, InitConfig initConfig)
public InfFlowProof(java.lang.String name, Term problem, java.lang.String header, InitConfig initConfig)
public InfFlowProof(java.lang.String name, InitConfig initConfig)
public InfFlowProofSymbols removeInfFlowProofSymbols()
public InfFlowProofSymbols getIFSymbols()
public void addIFSymbol(java.lang.Object s)
public void addLabeledIFSymbol(java.lang.Object s)
public void addTotalTerm(Term p)
public void addLabeledTotalTerm(Term p)
public void addGoalTemplates(Taclet t)
public void unionIFSymbols(InfFlowProofSymbols symbols)
public void unionLabeledIFSymbols(InfFlowProofSymbols symbols)
public java.lang.String printIFSymbols()
public boolean hasSideProofs()
public void addSideProof(InfFlowProof proof)
private void addSideProofStatistics(Statistics stat)
public SideProofStatistics getSideProofStatistics()