Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.nodeviews | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.symbolic_execution.profile | |
de.uka.ilkd.key.symbolic_execution.rule | |
org.key_project.ui.interactionlog |
Modifier and Type | Method and Description |
---|---|
ImmutableList<BuiltInRule> |
AbstractProofControl.getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<BuiltInRule> |
ProofControl.getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos)
collects all built-in rules that are applicable at the given sequent
position 'pos'.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<IBuiltInRuleApp> |
AbstractProofControl.getBuiltInRuleApp(Goal focusedGoal,
BuiltInRule rule,
PosInOccurrence pos)
collects all built-in rule applications for the given rule that are
applicable at position 'pos' and the current user constraint
|
void |
InteractionListener.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
void |
AbstractProofControl.selectedBuiltInRule(Goal goal,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
void |
ProofControl.selectedBuiltInRule(Goal goal,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced)
selected rule to apply
|
Constructor and Description |
---|
InfoTreeNode(BuiltInRule br,
java.util.Properties ruleExplanations) |
Modifier and Type | Method and Description |
---|---|
BuiltInRule |
BuiltInRuleMenuItem.connectedTo() |
BuiltInRule |
MenuItemForTwoModeRules.connectedTo() |
Constructor and Description |
---|
MenuItemForTwoModeRules(java.lang.String mainName,
java.lang.String actionTextForForcedMode,
java.lang.String tooltipForcedMode,
java.lang.String actionTextForInteractiveMode,
java.lang.String tooltipInteractiveMode,
BuiltInRule rule) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<BuiltInRule> |
BuiltInRuleIndex.rules()
returns all available rules
|
Constructor and Description |
---|
BuiltInRuleIndex(ImmutableList<BuiltInRule> rules)
creates a new index with the given built-in-rules
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<BuiltInRule> |
InitConfig.builtInRules()
returns the built-in rules of this initial configuration
|
ImmutableList<BuiltInRule> |
RuleCollection.getStandardBuiltInRules()
returns a list of all built in rules to be used
|
protected ImmutableList<BuiltInRule> |
JavaProfile.initBuiltInRules() |
protected ImmutableList<BuiltInRule> |
AbstractProfile.initBuiltInRules() |
Constructor and Description |
---|
RuleCollection(RuleSource standardTaclets,
ImmutableList<BuiltInRule> standardBuiltInRules) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractAuxiliaryContractRule
Rule for the application of
AuxiliaryContract s. |
class |
AbstractBlockContractRule
Rule for the application of
BlockContract s. |
class |
AbstractLoopContractRule
Rule for the application of
LoopContract s. |
class |
AbstractLoopInvariantRule
An abstract super class for loop invariant rules.
|
class |
BlockContractExternalRule
Rule for the application of
BlockContract s. |
class |
BlockContractInternalRule
Rule for the application of
BlockContract s. |
class |
LoopApplyHeadRule
This rule transforms a block that starts with a for loop into one that starts with a while loop.
|
class |
LoopContractExternalRule
Rule for the application of
LoopContract s. |
class |
LoopContractInternalRule
Rule for the application of
LoopContract s. |
class |
LoopScopeInvariantRule
Implementation of the "loop scope invariant" rule as
proposed in the PhD thesis by Nathan Wasser.
|
class |
OneStepSimplifier |
class |
QueryExpand
The QueryExpand rule allows to apply contracts or to symbolically execute a query
expression in the logic.
|
class |
UseDependencyContractRule |
class |
UseOperationContractRule
Implements the rule which inserts operation contracts for a method call.
|
class |
WhileInvariantRule |
Modifier and Type | Field and Description |
---|---|
protected BuiltInRule |
AbstractBuiltInRuleApp.builtInRule |
Modifier and Type | Method and Description |
---|---|
BuiltInRule |
IBuiltInRuleApp.rule()
returns the built in rule of this rule application
|
BuiltInRule |
AbstractBuiltInRuleApp.rule()
returns the rule of this rule application
|
Modifier and Type | Class and Description |
---|---|
class |
CloseAfterMerge
Rule for closing a partner goal after a merge operation.
|
class |
MergeRule
Base for implementing merge rules.
|
Constructor and Description |
---|
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio) |
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames) |
MergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio) |
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts) |
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Node mergeNode,
ImmutableList<MergePartner> mergePartners,
MergeProcedure concreteRule,
SymbolicExecutionStateWithProgCnt thisSEState,
ImmutableList<SymbolicExecutionState> mergePartnerStates,
Term distForm,
java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners) |
Modifier and Type | Class and Description |
---|---|
static class |
RuleAppSMT.SMTRule |
Modifier and Type | Method and Description |
---|---|
BuiltInRule |
RuleAppSMT.rule() |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<BuiltInRule> |
SymbolicExecutionJavaProfile.initBuiltInRules() |
Modifier and Type | Class and Description |
---|---|
class |
AbstractSideProofRule
Provides the basic functionality of
BuiltInRule which
computes something in a side proof. |
class |
ModalitySideProofRule
A
BuiltInRule which evaluates a modality in a side proof. |
class |
QuerySideProofRule
A
BuiltInRule which evaluates a query in a side proof. |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
Copyright © 2003-2019 The KeY-Project.