de.uka.ilkd.key.macros

Class PrepareInfFlowContractPreBranchesMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.PrepareInfFlowContractPreBranchesMacro

All Implemented Interfaces:

ProofMacro

public class PrepareInfFlowContractPreBranchesMacro
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	PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy 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.lang.String	AND_RIGHT_RULENAME
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
PrepareInfFlowContractPreBranchesMacro()

Method Summary

Modifier and Type	Method and Description
protected Strategy	createStrategy(Proof proof, PosInOccurrence posInOcc)
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.

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

applyTo, canApplyTo, doPostProcessing

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

AND_RIGHT_RULENAME

private static final java.lang.String AND_RIGHT_RULENAME

See Also:

Constant Field Values

Constructor Detail

PrepareInfFlowContractPreBranchesMacro

public PrepareInfFlowContractPreBranchesMacro()

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

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro