Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.tacletbuilder |
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) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<TacletAnnotation> |
Taclet.tacletAnnotations |
Modifier and Type | Method and Description |
---|---|
static TacletAnnotation |
TacletAnnotation.valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static TacletAnnotation[] |
TacletAnnotation.values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
Constructor and Description |
---|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
RewriteTaclet(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) |
RewriteTaclet(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)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<TacletAnnotation> |
TacletBuilder.tacletAnnotations |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.setAnnotations(ImmutableSet<TacletAnnotation> tacletAnnotations) |
Copyright © 2003-2019 The KeY-Project.