| 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 |
|---|---|
| AbstractAuxiliaryContractBuiltInRuleApp |
Application for
AbstractAuxiliaryContractRule. |
| AbstractAuxiliaryContractRule |
Rule for the application of
AuxiliaryContracts. |
| AbstractAuxiliaryContractRule.Instantiation |
This encapsulates all information from the rule application that is needed to apply the rule.
|
| AbstractAuxiliaryContractRule.Instantiator |
A builder for
AbstractAuxiliaryContractRule.Instantiations. |
| AbstractBlockContractBuiltInRuleApp |
Application of
AbstractBlockContractRule. |
| AbstractBlockContractRule |
Rule for the application of
BlockContracts. |
| AbstractBlockContractRule.BlockContractHint | |
| AbstractBlockContractRule.InfFlowValidityData | |
| AbstractBlockContractRule.Instantiator |
A builder for
Instantiations. |
| AbstractBuiltInRuleApp | |
| AbstractContractRuleApp | |
| AbstractLoopContractBuiltInRuleApp |
Application of
AbstractLoopContractRule. |
| AbstractLoopContractRule |
Rule for the application of
LoopContracts. |
| AbstractLoopContractRule.Instantiator |
A builder for
Instantiations. |
| AbstractLoopInvariantRule |
An abstract super class for loop invariant rules.
|
| AbstractLoopInvariantRule.AdditionalHeapTerms |
A container with data for the additional terms with assertions about the
heap; that is, the anonymizing update, the wellformed term, the frame
condition and the reachable state formula.
|
| AbstractLoopInvariantRule.AnonUpdateData |
A container containing data for the anonymizing update, that is the
actual update and the anonymized heap.
|
| AbstractLoopInvariantRule.Instantiation |
A container for an instantiation of this
LoopScopeInvariantRule
application; contains the update, the program with post condition, the
While loop the LoopScopeInvariantRule should be applied
to, the LoopSpecification, the the self Term. |
| AbstractLoopInvariantRule.LoopInvariantInformation |
A container object containing the information required for the concrete
loop invariant rules to create the sequents for the new goals.
|
| AntecTaclet |
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
| AuxiliaryContractBuilders |
This contains various builders used in building formulae and terms for block and loop contracts.
|
| AuxiliaryContractBuilders.ConditionsAndClausesBuilder |
This class is used to build various sub-formulas used in the block/loop contract rules.s
|
| AuxiliaryContractBuilders.GoalsConfigurator |
This class contains methods to add the premisses for the block contract rule to the goal.
|
| AuxiliaryContractBuilders.UpdatesBuilder |
This class is used to build the various updates that are needed for block/loop contract
rules.
|
| AuxiliaryContractBuilders.ValidityProgramConstructor |
This class is used to construct
block' from block (see Wacker 2012, 3.3). |
| AuxiliaryContractBuilders.VariablesCreatorAndRegistrar |
This class contains methods to create new variables from the contract's placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables()), and register them. |
| BlockContractExternalBuiltInRuleApp |
Application of
BlockContractExternalRule. |
| BlockContractExternalRule |
Rule for the application of
BlockContracts. |
| BlockContractInternalBuiltInRuleApp |
Application of
BlockContractInternalRule. |
| BlockContractInternalRule |
Rule for the application of
BlockContracts. |
| 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.
|
| IfFormulaInstantiationCache | |
| 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.
|
| IfMatchResult | |
| LoopApplyHeadBuiltInRuleApp |
Rule application for
LoopApplyHeadRule. |
| LoopApplyHeadRule |
This rule transforms a block that starts with a for loop into one that starts with a while loop.
|
| LoopContractExternalBuiltInRuleApp |
Application of
LoopContractExternalRule. |
| LoopContractExternalRule |
Rule for the application of
LoopContracts. |
| LoopContractInternalBuiltInRuleApp |
Application of
LoopContractInternalRule. |
| LoopContractInternalRule |
Rule for the application of
LoopContracts. |
| LoopInvariantBuiltInRuleApp |
The built in rule app for the loop invariant rule.
|
| LoopScopeInvariantRule |
Implementation of the "loop scope invariant" rule as
proposed in the PhD thesis by Nathan Wasser.
|
| 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 |
Instances of this class are used in the
Map of
OneStepSimplifier#replaceKnown(TermServices, SequentFormula, Map, List, Protocol)
to forece the same behavior as in Taclet rules where
names of logical variables and TermLabels are ignored. |
| 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
TermLabels. |
| 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.