Package de.uka.ilkd.key.rule

This package contains classes for implementing rules.

See: Description

Interface Summary

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 Summary

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 Summary

Enum	Description
Taclet.TacletLabelHint.TacletOperation	Defines the possible operations a Taclet performs.
TacletAnnotation	KeY parser can add annotations to taclets during parsing.

Exception Summary

Exception	Description
RuleAbortException

Package de.uka.ilkd.key.rule Description

This package contains classes for implementing rules. Most rules are taclet rules, represented by 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.