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.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
InfFlowContractAppTaclet
A normal RewriteTaclet except that the formula which is added by this taclet
is also added to the list of formulas contained in the
INF_FLOW_CONTRACT_APPL_PROPERTY.
|
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printRewriteAttributes(RewriteTaclet taclet) |
Modifier and Type | Method and Description |
---|---|
RewriteTaclet |
RewriteTaclet.setName(java.lang.String s) |
Modifier and Type | Method and Description |
---|---|
RewriteTacletExecutor<? extends RewriteTaclet> |
RewriteTaclet.getExecutor() |
Modifier and Type | Class and Description |
---|---|
class |
RewriteTacletExecutor<TacletKind extends RewriteTaclet> |
Modifier and Type | Class and Description |
---|---|
class |
RewriteTacletBuilder<T extends RewriteTaclet>
class builds RewriteTaclet objects.
|
Constructor and Description |
---|
RewriteTacletBuilderSchemaVarCollector(RewriteTacletBuilder<? extends RewriteTaclet> rtb) |
Modifier and Type | Method and Description |
---|---|
RewriteTaclet |
MethodWellDefinedness.combineTaclets(RewriteTaclet t1,
RewriteTaclet t2,
TermServices services)
Combines two well-definedness taclets for (pure) method invocations.
|
RewriteTaclet |
MethodWellDefinedness.createOperationTaclet(Services services)
Creates a well-definedness for a (pure) method invocation of this method.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<RewriteTaclet> |
ClassWellDefinedness.createInvTaclet(Services services)
Creates a well-definedness taclet for an invariant reference.
|
Modifier and Type | Method and Description |
---|---|
RewriteTaclet |
MethodWellDefinedness.combineTaclets(RewriteTaclet t1,
RewriteTaclet t2,
TermServices services)
Combines two well-definedness taclets for (pure) method invocations.
|
Copyright © 2003-2019 The KeY-Project.