Package | Description |
---|---|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.nparser.varexp | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule.tacletbuilder |
Modifier and Type | Method and Description |
---|---|
TacletBuilder |
TacletPBuilder.visitTriggers(KeYParser.TriggersContext ctx) |
Constructor and Description |
---|
TacletPBuilder(Services services,
NamespaceSet namespaces,
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilderCommand.apply(TacletBuilder<?> tacletBuilder,
java.lang.Object[] arguments,
java.util.List<java.lang.String> parameters,
boolean negated)
Applying this command on the given taclet builder.
|
default void |
ConditionBuilder.apply(TacletBuilder<?> tacletBuilder,
java.lang.Object[] arguments,
java.util.List<java.lang.String> parameters,
boolean negated)
This method will add the contructed
VariableCondition to given tacletBuilder . |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> |
InitConfig.getTaclet2Builder()
Taclet s are constructed using TacletBuilder s this map
contains the pair of a taclet and its builder which is important as
goals of a taclet may depend of the selected choices. |
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.setTaclet2Builder(java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
Modifier and Type | Class and Description |
---|---|
class |
AntecTacletBuilder
class builds Schematic Theory Specific Rules (Taclets) with find part
int antecedent.
|
class |
FindTacletBuilder<T extends FindTaclet>
Superclass of TacletBuilder objects that have a non-empty find clause.
|
class |
NoFindTacletBuilder
Due to the immutability of
Taclet s, they are created in the parsers
using TacletBuilder s. |
class |
RewriteTacletBuilder<T extends RewriteTaclet>
class builds RewriteTaclet objects.
|
class |
SuccTacletBuilder
class builds SuccTaclet objects.
|
Constructor and Description |
---|
TacletBuilderException(TacletBuilder<?> tb,
java.lang.String errorMessage) |
TacletPrefixBuilder(TacletBuilder<? extends Taclet> tacletBuilder) |
Copyright © 2003-2019 The KeY-Project.