Class and Description |
---|
IfFormulaInstantiation |
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
RuleApp |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
IfFormulaInstantiation |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
RuleSet |
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
Rule |
RuleAbortException |
Class and Description |
---|
Rule |
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
IBuiltInRuleApp |
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
PosTacletApp
A position taclet application object, contains already the information to
which term/formula of the sequent the taclet is attached.
|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
RuleApp |
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
FindTaclet
An abstract class to represent Taclets with a find part.
|
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
Rule |
RuleSet |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletAnnotation
KeY parser can add annotations to taclets during parsing.
|
TacletApplPart |
TacletAttributes |
TacletPrefix |
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
RuleApp |
Taclet.TacletLabelHint
Instances of this class are used as hints to maintain
TermLabel s. |
Class and Description |
---|
IfFormulaInstantiationCache |
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
AbstractProgramElement |
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
AbstractProgramElement |
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
RuleSet |
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
Rule |
RuleApp |
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
RuleSet |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
VariableCondition
The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables.
|
Class and Description |
---|
NewVarcond
variable condition used if a new variable is introduced
|
NotFreeIn |
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
RuleSet |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
VariableCondition
The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables.
|
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
NoPosTacletApp
A no position taclet application has no position information yet.
|
RuleApp |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
NoPosTacletApp
A no position taclet application has no position information yet.
|
RuleApp |
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
NoPosTacletApp
A no position taclet application has no position information yet.
|
OneStepSimplifier |
Rule |
RuleApp |
RuleSet |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
IfFormulaInstantiation |
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
Rule |
RuleApp |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
Rule |
RuleSet |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
AbstractAuxiliaryContractBuiltInRuleApp
Application for
AbstractAuxiliaryContractRule . |
AbstractAuxiliaryContractRule
Rule for the application of
AuxiliaryContract s. |
AbstractAuxiliaryContractRule.Instantiation
This encapsulates all information from the rule application that is needed to apply the rule.
|
AbstractAuxiliaryContractRule.Instantiator
A builder for
AbstractAuxiliaryContractRule.Instantiation s. |
AbstractBlockContractBuiltInRuleApp
Application of
AbstractBlockContractRule . |
AbstractBlockContractRule
Rule for the application of
BlockContract s. |
AbstractBlockContractRule.BlockContractHint |
AbstractBlockContractRule.InfFlowValidityData |
AbstractBuiltInRuleApp |
AbstractContractRuleApp |
AbstractLoopContractBuiltInRuleApp
Application of
AbstractLoopContractRule . |
AbstractLoopContractRule
Rule for the application of
LoopContract s. |
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.
|
BlockContractExternalBuiltInRuleApp
Application of
BlockContractExternalRule . |
BlockContractExternalRule
Rule for the application of
BlockContract s. |
BlockContractInternalBuiltInRuleApp
Application of
BlockContractInternalRule . |
BlockContractInternalRule
Rule for the application of
BlockContract s. |
BuiltInRule
Buit-in rule interface.
|
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.
|
IBuiltInRuleApp |
IfFormulaInstantiation |
IfMatchResult |
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
LoopContract s. |
LoopContractInternalBuiltInRuleApp
Application of
LoopContractInternalRule . |
LoopContractInternalRule
Rule for the application of
LoopContract s. |
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.Protocol |
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.
|
Rule |
RuleAbortException |
RuleApp |
RuleSet |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
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. |
Taclet.TacletLabelHint.TacletOperation
Defines the possible operations a
Taclet performs. |
TacletAnnotation
KeY parser can add annotations to taclets during parsing.
|
TacletApp
A TacletApp object contains information required for a concrete application.
|
TacletApplPart |
TacletAttributes |
TacletMatcher |
TacletPrefix |
TacletSchemaVariableCollector
Collects all schemavariables occurring in the
\find, \assumes part or goal description of a taclet. |
Trigger |
UseDependencyContractApp |
UseDependencyContractRule |
UseOperationContractRule
Implements the rule which inserts operation contracts for a method call.
|
UseOperationContractRule.Instantiation |
VariableCondition
The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables.
|
WhileInvariantRule |
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
VariableCondition
The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables.
|
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.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
AntecTaclet
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
FindTaclet
An abstract class to represent Taclets with a find part.
|
IfFormulaInstantiation |
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
NoFindTaclet
Used to implement a Taclet that has no find part.
|
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
RuleApp |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
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.
|
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
Rule |
RuleApp |
Taclet.TacletLabelHint
Instances of this class are used as hints to maintain
TermLabel s. |
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletMatcher |
Class and Description |
---|
IfFormulaInstantiation |
IfMatchResult |
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletMatcher |
Class and Description |
---|
IfFormulaInstantiation |
IfMatchResult |
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletMatcher |
Class and Description |
---|
MatchConditions
Simple container class containing the information resulting from a
Taclet.match-call
|
Class and Description |
---|
AbstractBuiltInRuleApp |
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
Rule |
RuleAbortException |
RuleApp |
Class and Description |
---|
Rule |
RuleApp |
Class and Description |
---|
AntecTaclet
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
FindTaclet
An abstract class to represent Taclets with a find part.
|
NewDependingOn
Deprecated.
|
NewVarcond
variable condition used if a new variable is introduced
|
NoFindTaclet
Used to implement a Taclet that has no find part.
|
NotFreeIn |
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
RuleSet |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletAnnotation
KeY parser can add annotations to taclets during parsing.
|
TacletAttributes |
TacletPrefix |
Trigger |
VariableCondition
The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables.
|
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
AbstractBuiltInRuleApp |
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
Rule |
RuleApp |
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
IfFormulaInstantiation |
NoPosTacletApp
A no position taclet application has no position information yet.
|
RuleApp |
RuleSet |
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
RuleApp |
RuleSet |
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
Rule |
RuleApp |
SyntacticalReplaceVisitor |
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.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
RuleApp |
Class and Description |
---|
RuleApp |
Class and Description |
---|
RuleApp |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
RuleApp |
Class and Description |
---|
LoopInvariantBuiltInRuleApp
The built in rule app for the loop invariant rule.
|
RuleApp |
UseOperationContractRule.Instantiation |
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
Rule |
RuleAbortException |
RuleApp |
Class and Description |
---|
RuleApp |
Class and Description |
---|
RuleApp |
Class and Description |
---|
RuleApp |
TacletApp
A TacletApp object contains information required for a concrete application.
|
Class and Description |
---|
FindTaclet
An abstract class to represent Taclets with a find part.
|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
IBuiltInRuleApp |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
OneStepSimplifier |
RuleApp |
Class and Description |
---|
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Class and Description |
---|
BuiltInRule
Buit-in rule interface.
|
IBuiltInRuleApp |
RuleApp |
Class and Description |
---|
RuleApp |
Class and Description |
---|
ContractRuleApp
Represents an application of a contract rule.
|
IBuiltInRuleApp |
LoopContractInternalBuiltInRuleApp
Application of
LoopContractInternalRule . |
LoopInvariantBuiltInRuleApp
The built in rule app for the loop invariant rule.
|
OneStepSimplifierRuleApp |
UseDependencyContractApp |
Copyright © 2003-2019 The KeY-Project.