public class UseInformationFlowContractMacro extends StrategyProofMacro
ADMITTED_RULENAMES
.
Modifier and Type | Class and Description |
---|---|
protected class |
UseInformationFlowContractMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
ProofMacro.ProgressBarListener
Constructor and Description |
---|
UseInformationFlowContractMacro() |
Modifier and Type | Method and Description |
---|---|
protected static java.util.Set<java.lang.String> |
asSet(java.lang.String[] strings) |
protected UseInformationFlowContractMacro.PropExpansionStrategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected void |
doPostProcessing(Proof proof)
Subclasses can use this method to do some postprocessing on the
proof-object after the strategy has finished.
|
protected java.util.Set<java.lang.String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
protected boolean |
ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
applyTo, canApplyTo
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getDescription()
ProofMacro
null
constant stringprotected java.util.Set<java.lang.String> getAdmittedRuleNames()
null
setprotected static java.util.Set<java.lang.String> asSet(java.lang.String[] strings)
protected UseInformationFlowContractMacro.PropExpansionStrategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal)
ruleApp
- rule to be appliedpio
- contextgoal
- contextprotected void doPostProcessing(Proof proof)
StrategyProofMacro
doPostProcessing
in class StrategyProofMacro
proof
- The proof object.Copyright © 2003-2019 The KeY-Project.