Interface | Description |
---|---|
AbstractProgramElement | |
BuiltInRule |
Buit-in rule interface.
|
IBuiltInRuleApp | |
IfFormulaInstantiation | |
Rule | |
RuleApp | |
TacletMatcher | |
VariableCondition |
The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables.
|
Class | Description |
---|---|
AbstractBuiltInRuleApp | |
AbstractContractRuleApp | |
AntecTaclet |
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
BlockContractBuiltInRuleApp | |
BlockContractRule | |
BlockContractRule.ConditionsAndClausesBuilder | |
BlockContractRule.GoalsConfigurator | |
BlockContractRule.Instantiation | |
BlockContractRule.Instantiator | |
BlockContractRule.UpdatesBuilder | |
BlockContractRule.ValidityProgramConstructor | |
BlockContractRule.VariablesCreatorAndRegistrar | |
BoundUniquenessChecker |
The bound uniqueness checker ensures that schemavariables can be bound
at most once in the \find and \assumes part of a taclet.
|
ContractRuleApp |
Represents an application of a contract rule.
|
DefaultBuiltInRuleApp |
this class represents an application of a built in rule
application
|
FindTaclet |
An abstract class to represent Taclets with a find part.
|
IfFormulaInstDirect |
Instantiation of an if-formula that has to be proven by an explicit
if-goal
|
IfFormulaInstSeq |
Instantiation of an if-formula that is a formula of an existing
sequent.
|
IfFormulaInstSeq.Cache | |
IfMatchResult | |
LoopInvariantBuiltInRuleApp |
The built in rule app for the loop invariant rule.
|
MatchConditions |
Simple container class containing the information resulting from a
Taclet.match-call
|
NewDependingOn | Deprecated |
NewVarcond |
variable condition used if a new variable is introduced
|
NoFindTaclet |
Used to implement a Taclet that has no find part.
|
NoPosTacletApp |
A no position taclet application has no position information yet.
|
NotFreeIn | |
OneStepSimplifier | |
OneStepSimplifier.Instantiation | |
OneStepSimplifier.Protocol | |
OneStepSimplifier.TermReplacementKey | |
OneStepSimplifierRuleApp | |
PosTacletApp |
A position taclet application object, contains already the information to
which term/formula of the sequent the taclet is attached.
|
QueryExpand |
The QueryExpand rule allows to apply contracts or to symbolically execute a query
expression in the logic.
|
RewriteTaclet |
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
RuleKey |
Provides a unique key for taclets based on a taclet's name and its taclet options.
|
RuleSet | |
SuccTaclet |
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
SVNameCorrespondenceCollector |
This visitor is used to collect information about schema variable
pairs occurring within the same substitution operator within a
taclet.
|
SyntacticalReplaceVisitor | |
Taclet |
Taclets are the DL-extension of schematic theory specific rules.
|
Taclet.TacletLabelHint |
Instances of this class are used as hints to maintain
TermLabel s. |
TacletApp |
A TacletApp object contains information required for a concrete application.
|
TacletApplPart | |
TacletAttributes | |
TacletPrefix | |
TacletSchemaVariableCollector |
Collects all schemavariables occurring in the
\find, \assumes part or goal description of a taclet. |
TacletVariableSVCollector |
This class is used to collect all appearing SchemaVariables that are bound in a
Taclet.
|
Trigger | |
UninstantiatedNoPosTacletApp |
A subclass of
NoPosTacletApp for the special case of a
taclet app without any instantiations. |
UseDependencyContractApp | |
UseDependencyContractRule | |
UseOperationContractRule |
Implements the rule which inserts operation contracts for a method call.
|
UseOperationContractRule.AnonUpdateData | |
UseOperationContractRule.Instantiation | |
VariableConditionAdapter |
The variable condition adapter can be used by variable conditions
which can either fail or be successful, but which do not create a
constraint.
|
WhileInvariantRule | |
WhileInvariantRule.AnonUpdateData | |
WhileInvariantRule.InfFlowData | |
WhileInvariantRule.Instantiation |
Enum | Description |
---|---|
Taclet.TacletLabelHint.TacletOperation |
Defines the possible operations a
Taclet performs. |
TacletAnnotation |
KeY parser can add annotations to taclets during parsing.
|
Exception | Description |
---|---|
RuleAbortException |
Taclet
. The package includes the
representation of applications of taclets (TacletApp
) and the builders of taclets (de.uka.ilkd.key.rule.TacletBuilder
). Besides taclets, there are
built-in rules implemented directly in Java.