Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
org.key_project.util.collection |
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) |
Constructor and Description |
---|
RenameTable(RenameTable parent,
ImmutableMap<QuantifiableVariable,java.lang.Integer> localTable,
int newMax) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableMap<SchemaVariable,TacletPrefix> |
Taclet.prefixMap
map from a schemavariable to its prefix.
|
Modifier and Type | Method and Description |
---|---|
ImmutableMap<SchemaVariable,SchemaVariable> |
SVNameCorrespondenceCollector.getCorrespondences() |
ImmutableMap<SchemaVariable,TacletPrefix> |
Taclet.prefixMap() |
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 |
---|---|
ImmutableMap<GenericSort,Sort> |
GenericSortInstantiations.getAllInstantiations()
ONLY FOR JUNIT TESTS
|
ImmutableMap<SchemaVariable,Term> |
TacletInstantiations.instantiations() |
ImmutableMap<SchemaVariable,InstantiationEntry<?>> |
SVInstantiations.interesting() |
Constructor and Description |
---|
TacletInstantiations(Taclet rule,
ImmutableMap<SchemaVariable,Term> instantiations) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableMap<SchemaVariable,TacletPrefix> |
TacletPrefixBuilder.prefixMap |
Modifier and Type | Method and Description |
---|---|
ImmutableMap<SchemaVariable,TacletPrefix> |
TacletPrefixBuilder.getPrefixMap() |
Modifier and Type | Method and Description |
---|---|
ImmutableMap<QuantifiableVariable,Term> |
Substitution.getVarMap() |
Constructor and Description |
---|
Substitution(ImmutableMap<QuantifiableVariable,Term> map) |
Modifier and Type | Class and Description |
---|---|
class |
DefaultImmutableMap<S,T>
This class implements ImmMap
|
Modifier and Type | Method and Description |
---|---|
ImmutableMap<S,T> |
DefaultImmutableMap.put(S key,
T value)
inserts mapping
null is not allowed for key or value. |
ImmutableMap<S,T> |
ImmutableMap.put(S key,
T value)
adds a mapping
|
ImmutableMap<S,T> |
ImmutableMap.remove(S key)
removes mapping (key,...) from map
|
ImmutableMap<S,T> |
DefaultImmutableMap.removeAll(T value)
removes all mappings (...,value) from map
|
ImmutableMap<S,T> |
ImmutableMap.removeAll(T value)
removes all mappings (...,value) from map
|
Copyright © 2003-2019 The KeY-Project.