Package | Description |
---|---|
de.uka.ilkd.key.core | |
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.nparser | |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.settings | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
Namespace<Choice> |
KeYMediator.choice_ns()
returns the choice namespace
|
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 |
---|---|
Namespace<Choice> |
NamespaceSet.choices() |
Modifier and Type | Method and Description |
---|---|
void |
NamespaceSet.setChoices(Namespace<Choice> choiceNS) |
Constructor and Description |
---|
NamespaceSet(Namespace<QuantifiableVariable> varNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS,
Namespace<RuleSet> ruleSetNS,
Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Choice> |
ChoiceInformation.getActivatedChoices() |
Namespace<Choice> |
ChoiceInformation.getChoices() |
Constructor and Description |
---|
ChoiceInformation(Namespace<Choice> choices) |
Modifier and Type | Method and Description |
---|---|
Choice |
ChoiceFinder.visitActivated_choice(KeYParser.Activated_choiceContext ctx) |
Choice |
TacletPBuilder.visitOption(KeYParser.OptionContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<Choice> |
DefaultBuilder.choices() |
java.util.List<Choice> |
TacletPBuilder.visitOption_list(KeYParser.Option_listContext ctx) |
Constructor and Description |
---|
ChoiceFinder(Namespace<Choice> choices) |
Modifier and Type | Method and Description |
---|---|
Namespace<Choice> |
InitConfig.choiceNS()
returns the choice namespace of this initial configuration
|
ImmutableSet<Choice> |
InitConfig.getActivatedChoices()
Returns the choices which are currently active.
|
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.setActivatedChoices(ImmutableSet<Choice> activatedChoices)
sets the set of activated choices of this initial configuration.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<Choice> |
Taclet.choices
the set of taclet options for this taclet
|
ImmutableSet<Choice> |
RuleKey.choices |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Choice> |
Taclet.getChoices() |
ImmutableSet<Choice> |
Taclet.getTacletOptions() |
Modifier and Type | Method and Description |
---|---|
void |
Taclet.setTacletOptions(ImmutableSet<Choice> tacletOptions) |
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<Choice> |
TacletBuilder.choices |
protected java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
TacletBuilder.goal2Choices |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Choice> |
TacletBuilder.getChoices() |
java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
TacletBuilder.getGoal2Choices() |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addGoal2ChoicesMapping(TacletGoalTemplate gt,
ImmutableSet<Choice> soc)
adds a mapping from GoalTemplate
gt to SetOfsoc |
T |
TacletBuilder.getTacletWithoutInactiveGoalTemplates(ImmutableSet<Choice> active) |
void |
TacletBuilder.setChoices(ImmutableSet<Choice> choices) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Choice> |
ChoiceSettings.getDefaultChoicesAsSet()
returns the current selected choices as set
|
Modifier and Type | Method and Description |
---|---|
void |
ChoiceSettings.updateChoices(Namespace<Choice> choiceNS,
boolean remove)
updates
category2Choices if new entries are found
in choiceNS or if entries of category2Choices
are no longer present in choiceNS |
ChoiceSettings |
ChoiceSettings.updateWith(java.lang.Iterable<Choice> sc) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Choice> |
SideProofUtil.activateChoice(ImmutableSet<Choice> choices,
Choice choiceToActivate)
removes all choices with the same category as
choiceToActivate from
choices and adds choiceToActivate to the set |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Choice> |
SideProofUtil.activateChoice(ImmutableSet<Choice> choices,
Choice choiceToActivate)
removes all choices with the same category as
choiceToActivate from
choices and adds choiceToActivate to the set |
static ProofEnvironment |
SideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
Choice... enableChoices)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Choice> |
SideProofUtil.activateChoice(ImmutableSet<Choice> choices,
Choice choiceToActivate)
removes all choices with the same category as
choiceToActivate from
choices and adds choiceToActivate to the set |
Copyright © 2003-2019 The KeY-Project.