de.uka.ilkd.key.informationflow.macros

Class UseInformationFlowContractMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.informationflow.macros.UseInformationFlowContractMacro

All Implemented Interfaces:

ProofMacro

public class UseInformationFlowContractMacro
extends StrategyProofMacro

The macro UseInformationFlowContractMacro applies all applicable information flow contracts.

The rules that are applied can be set in ADMITTED_RULENAMES.

Author:

christoph

Nested Class Summary

Nested Classes

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.

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
UseInformationFlowContractMacro()

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.macros.StrategyProofMacro

applyTo, canApplyTo

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

INF_FLOW_RULENAME_PREFIX

private static final java.lang.String INF_FLOW_RULENAME_PREFIX

See Also:

Constant Field Values

IMP_LEFT_RULENAME

private static final java.lang.String IMP_LEFT_RULENAME

See Also:

Constant Field Values

DOUBLE_IMP_LEFT_RULENAME

private static final java.lang.String DOUBLE_IMP_LEFT_RULENAME

See Also:

Constant Field Values

ADMITTED_RULENAMES

private static final java.lang.String[] ADMITTED_RULENAMES

ADMITTED_RULENAME_SET

private static final java.util.Set<java.lang.String> ADMITTED_RULENAME_SET

appliedInfFlowRules

private static ImmutableSet<java.lang.String> appliedInfFlowRules

Constructor Detail

UseInformationFlowContractMacro

public UseInformationFlowContractMacro()

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofMacro

Gets the name of this macro. Used as menu entry

Returns:

a non-null constant string

getCategory

public java.lang.String getCategory()

Description copied from interface: ProofMacro

Gets the category of this macro. Used as name of the menu under which the macro is sorted. Return null if no submenu is to be created.

Returns:

a constant string, or null

getDescription

public java.lang.String getDescription()

Description copied from interface: ProofMacro

Gets the description of this macro. Used as tooltip.

Returns:

a non-null constant string

getAdmittedRuleNames

protected java.util.Set<java.lang.String> getAdmittedRuleNames()

Gets the set of admitted rule names.

Returns:

a constant non- null set

asSet

protected static java.util.Set<java.lang.String> asSet(java.lang.String[] strings)

createStrategy

protected UseInformationFlowContractMacro.PropExpansionStrategy createStrategy(Proof proof,
                                                                               PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro

ruleApplicationInContextAllowed

protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp,
                                                  PosInOccurrence pio,
                                                  Goal goal)

Checks whether the application of the passed rule is ok in the given context.

Parameters:

ruleApp - rule to be applied

pio - context

goal - context

Returns:

true if rule may be applied

doPostProcessing

protected void doPostProcessing(Proof proof)

Description copied from class: StrategyProofMacro

Subclasses can use this method to do some postprocessing on the proof-object after the strategy has finished.

Overrides:

doPostProcessing in class StrategyProofMacro

Parameters:

proof - The proof object.

getAppRuleName

private java.lang.String getAppRuleName(Node parent)