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
Modifier and Type | Field and Description |
---|---|
private static Set<String> |
ADMITTED_RULENAME_SET |
private static String[] |
ADMITTED_RULENAMES |
private static ImmutableSet<String> |
appliedInfFlowRules |
private static String |
DOUBLE_IMP_LEFT_RULENAME |
private static String |
IMP_LEFT_RULENAME |
private static String |
INF_FLOW_RULENAME_PREFIX |
Constructor and Description |
---|
UseInformationFlowContractMacro() |
Modifier and Type | Method and Description |
---|---|
protected static Set<String> |
asSet(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 Set<String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
private String |
getAppRuleName(Node parent) |
String |
getCategory()
Gets the category of this macro.
|
String |
getDescription()
Gets the description of this macro.
|
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
private static final String INF_FLOW_RULENAME_PREFIX
private static final String IMP_LEFT_RULENAME
private static final String DOUBLE_IMP_LEFT_RULENAME
private static final String[] ADMITTED_RULENAMES
private static ImmutableSet<String> appliedInfFlowRules
public String getName()
ProofMacro
null
constant stringpublic String getCategory()
ProofMacro
null
if no submenu is to be created.null
public String getDescription()
ProofMacro
null
constant stringprotected Set<String> getAdmittedRuleNames()
null
setprotected 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.