Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule | |
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.taclettranslation |
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 | Class and Description |
---|---|
class |
AntecTaclet
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
class |
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
class |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
Modifier and Type | Method and Description |
---|---|
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
MatchConditions matchCond,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos,
Services services)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
Modifier and Type | Class and Description |
---|---|
class |
FindTacletExecutor<TacletKind extends FindTaclet> |
Modifier and Type | Class and Description |
---|---|
class |
FindTacletBuilder<T extends FindTaclet>
Superclass of TacletBuilder objects that have a non-empty find clause.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
DefaultTacletTranslator.getFindFromTaclet(FindTaclet findTaclet)
Retrieve the "find" Term from a FindTaclet.
|
Copyright © 2003-2019 The KeY-Project.