de.uka.ilkd.key.informationflow.rule

Class InfFlowContractAppTaclet

java.lang.Object

de.uka.ilkd.key.rule.Taclet

de.uka.ilkd.key.rule.FindTaclet

de.uka.ilkd.key.rule.RewriteTaclet

de.uka.ilkd.key.informationflow.rule.InfFlowContractAppTaclet

All Implemented Interfaces:

Named, Rule

public class InfFlowContractAppTaclet
extends RewriteTaclet

A normal RewriteTaclet except that the formula which is added by this taclet is also added to the list of formulas contained in the INF_FLOW_CONTRACT_APPL_PROPERTY. The INF_FLOW_CONTRACT_APPL_PROPERTY is used by the macros UseInformationFlowContractMacro and PrepareInfFlowContractPreBranchesMacro to decide how to prepare the formulas resulting from information flow contract applications.

Author:

christoph

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.Taclet

Taclet.TacletLabelHint

Field Summary

Fields

Modifier and Type	Field and Description
private static ImmutableSet<Name>	alreadyRegistered
static java.lang.String	USE_IF

Fields inherited from class de.uka.ilkd.key.rule.RewriteTaclet

ANTECEDENT_POLARITY, IN_SEQUENT_STATE, NONE, SAME_UPDATE_LEVEL, SUCCEDENT_POLARITY

Fields inherited from class de.uka.ilkd.key.rule.FindTaclet

find

Fields inherited from class de.uka.ilkd.key.rule.Taclet

choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString

Constructor Summary

Constructors

Constructor and Description
InfFlowContractAppTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, int p_applicationRestriction, ImmutableSet<Choice> choices, boolean surviveSymbExec, ImmutableSet<TacletAnnotation> tacletAnnotations)
InfFlowContractAppTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, int p_applicationRestriction, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations)

Method Summary

Modifier and Type	Method and Description
protected void	createAndInitializeExecutor()
static boolean	hasType(Rule rule)
static void	register(Name name)
static boolean	registered(Name name)
InfFlowContractAppTaclet	setName(java.lang.String s)
static boolean	unregister(Name name)

Methods inherited from class de.uka.ilkd.key.rule.RewriteTaclet

checkPrefix, getApplicationRestriction, getExecutor, getRewriteResult, ignoreTopLevelUpdates, toStringFind

Methods inherited from class de.uka.ilkd.key.rule.FindTaclet

equals, find, getBoundVariablesHelper, getIfFindVariables, hashCode, toString

Methods inherited from class de.uka.ilkd.key.rule.Taclet

admissible, admissibleAutomatic, admissibleInteractive, apply, closeGoal, collectSchemaVars, createAndInitializeMatcher, createTacletServices, displayName, getBoundVariables, getChoices, getIfVariables, getMatcher, getNameCorrespondent, getPrefix, getRuleJustification, getRuleSets, getSurviveSymbExec, getTrigger, getVariableConditions, goalTemplates, hasReplaceWith, hasTrigger, ifSequent, isContextInPrefix, name, prefixMap, ruleSets, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

USE_IF

public static final java.lang.String USE_IF

See Also:

Constant Field Values

alreadyRegistered

private static ImmutableSet<Name> alreadyRegistered

Constructor Detail

InfFlowContractAppTaclet

public InfFlowContractAppTaclet(Name name,
                                TacletApplPart applPart,
                                ImmutableList<TacletGoalTemplate> goalTemplates,
                                ImmutableList<RuleSet> ruleSets,
                                TacletAttributes attrs,
                                Term find,
                                ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
                                int p_applicationRestriction,
                                ImmutableSet<Choice> choices,
                                ImmutableSet<TacletAnnotation> tacletAnnotations)

InfFlowContractAppTaclet

public InfFlowContractAppTaclet(Name name,
                                TacletApplPart applPart,
                                ImmutableList<TacletGoalTemplate> goalTemplates,
                                ImmutableList<RuleSet> ruleSets,
                                TacletAttributes attrs,
                                Term find,
                                ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
                                int p_applicationRestriction,
                                ImmutableSet<Choice> choices,
                                boolean surviveSymbExec,
                                ImmutableSet<TacletAnnotation> tacletAnnotations)

Method Detail

hasType

public static boolean hasType(Rule rule)

registered

public static boolean registered(Name name)

register

public static void register(Name name)

unregister

public static boolean unregister(Name name)

createAndInitializeExecutor

protected void createAndInitializeExecutor()

Overrides:

createAndInitializeExecutor in class RewriteTaclet

setName

public InfFlowContractAppTaclet setName(java.lang.String s)

Overrides:

setName in class RewriteTaclet