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 java.util.Set<java.lang.String> |
ADMITTED_RULENAME_SET |
private static java.lang.String[] |
ADMITTED_RULENAMES |
private static ImmutableSet<java.lang.String> |
appliedInfFlowRules |
private static java.lang.String |
DOUBLE_IMP_LEFT_RULENAME |
private static java.lang.String |
IMP_LEFT_RULENAME |
private static java.lang.String |
INF_FLOW_RULENAME_PREFIX |
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.
|
private java.lang.String |
getAppRuleName(Node parent) |
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
private static final java.lang.String INF_FLOW_RULENAME_PREFIX
private static final java.lang.String IMP_LEFT_RULENAME
private static final java.lang.String DOUBLE_IMP_LEFT_RULENAME
private static final java.lang.String[] ADMITTED_RULENAMES
private static final java.util.Set<java.lang.String> ADMITTED_RULENAME_SET
private static ImmutableSet<java.lang.String> appliedInfFlowRules
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.private java.lang.String getAppRuleName(Node parent)