Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.symbolic_execution |
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 | Method and Description |
---|---|
protected void |
LogicPrinter.printGoalTemplate(TacletGoalTemplate tgt) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TacletGoalTemplate> |
Taclet.goalTemplates()
returns an iterator over the goal descriptions.
|
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 | Method and Description |
---|---|
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
Modifier and Type | Class and Description |
---|---|
class |
AntecSuccTacletGoalTemplate |
class |
RewriteTacletGoalTemplate
this class inherits from TacletGoalTemplate.
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
TacletBuilder.goal2Choices |
protected ImmutableList<TacletGoalTemplate> |
TacletBuilder.goals |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
TacletBuilder.getGoal2Choices() |
ImmutableList<TacletGoalTemplate> |
TacletBuilder.goalTemplates() |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addGoal2ChoicesMapping(TacletGoalTemplate gt,
ImmutableSet<Choice> soc)
adds a mapping from GoalTemplate
gt to SetOfsoc |
void |
AntecTacletBuilder.addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
abstract void |
TacletBuilder.addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
void |
SuccTacletBuilder.addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
void |
RewriteTacletBuilder.addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
void |
NoFindTacletBuilder.addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.setTacletGoalTemplates(ImmutableList<TacletGoalTemplate> g) |
Modifier and Type | Method and Description |
---|---|
protected static void |
TruthValueTracingUtil.analyzeTacletGoal(Node parent,
TacletApp tacletApp,
TacletGoalTemplate tacletGoal,
java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> labels,
Services services,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Analyzes the given
TacletGoalTemplate . |
Copyright © 2003-2019 The KeY-Project.