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.mergerule | |
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.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.rule | |
de.uka.ilkd.key.ui | |
org.key_project.ui.interactionlog | |
org.key_project.ui.interactionlog.model.builtin |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced)
completes rule applications of built in rules
|
protected IBuiltInRuleApp |
AbstractProofControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
static IBuiltInRuleApp |
AbstractProofControl.completeBuiltInRuleAppByDefault(IBuiltInRuleApp app,
Goal goal,
boolean forced)
Default implementation of
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp, Goal, boolean) . |
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
|
protected ImmutableSet<IBuiltInRuleApp> |
AbstractProofControl.getBuiltInRuleAppsForName(Goal focusedGoal,
java.lang.String name,
PosInOccurrence pos)
collects all applications of a rule given by its name at a give position
in the sequent
|
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced)
completes rule applications of built in rules
|
protected IBuiltInRuleApp |
AbstractProofControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
static IBuiltInRuleApp |
AbstractProofControl.completeBuiltInRuleAppByDefault(IBuiltInRuleApp app,
Goal goal,
boolean forced)
Default implementation of
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp, Goal, boolean) . |
void |
InteractionListener.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
LoopContractExternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
LoopApplyHeadCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
BlockContractInternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
InteractiveRuleApplicationCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced)
method called to complete the given builtin rule application
|
IBuiltInRuleApp |
BlockContractExternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
LoopInvariantRuleCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
FunctionalOperationContractCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
LoopContractInternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
DependencyContractCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
WindowUserInterfaceControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
boolean |
LoopContractExternalCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
LoopApplyHeadCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
BlockContractInternalCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
InteractiveRuleApplicationCompletion.canComplete(IBuiltInRuleApp app)
checks if this instance is responsible for the given app
|
boolean |
BlockContractExternalCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
LoopInvariantRuleCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
FunctionalOperationContractCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
LoopContractInternalCompletion.canComplete(IBuiltInRuleApp app) |
boolean |
DependencyContractCompletion.canComplete(IBuiltInRuleApp app) |
static boolean |
LoopContractExternalCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
static boolean |
BlockContractInternalCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
static boolean |
BlockContractExternalCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
static boolean |
LoopInvariantRuleCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
static boolean |
FunctionalOperationContractCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
static boolean |
LoopContractInternalCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
static boolean |
DependencyContractCompletion.checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
IBuiltInRuleApp |
LoopContractExternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
LoopApplyHeadCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
BlockContractInternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
InteractiveRuleApplicationCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced)
method called to complete the given builtin rule application
|
IBuiltInRuleApp |
BlockContractExternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
LoopInvariantRuleCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
FunctionalOperationContractCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
LoopContractInternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
DependencyContractCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
WindowUserInterfaceControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
MergeRuleCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
boolean |
MergeRuleCompletion.canComplete(IBuiltInRuleApp app) |
static boolean |
MergeRuleCompletion.checkCanComplete(IBuiltInRuleApp app) |
IBuiltInRuleApp |
MergeRuleCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<IBuiltInRuleApp> |
BuiltInRuleAppIndex.getBuiltInRule(Goal goal,
PosInOccurrence pos)
returns a list of built-in rules application applicable
for the given goal and position
|
ImmutableList<IBuiltInRuleApp> |
RuleAppIndex.getBuiltInRules(Goal g,
PosInOccurrence pos)
returns a list of built-in rule applications applicable
for the given goal, user defined constraint and position
|
Modifier and Type | Class and Description |
---|---|
class |
CloseAfterMergeRuleBuiltInRuleApp
Rule application class for close-after-merge rule applications.
|
class |
MergeRuleBuiltInRuleApp
Rule application class for merge rule applications.
|
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
MergeRule.createApp(PosInOccurrence pio,
TermServices services) |
IBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
CloseAfterMergeRuleBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
MergeRuleBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
Modifier and Type | Class and Description |
---|---|
class |
RuleAppSMT
The rule application that is used when a goal is closed by means of an external solver.
|
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
ModalitySideProofRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
QuerySideProofRule.createApp(PosInOccurrence pos,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
ConsoleUserInterfaceControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
ConsoleUserInterfaceControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
Modifier and Type | Method and Description |
---|---|
static <T extends IBuiltInRuleApp> |
BuiltInRuleInteractionFactory.create(Node node,
T app) |
static <T extends IBuiltInRuleApp> |
BuiltInRuleInteractionFactory.get(T app) |
static <T extends IBuiltInRuleApp> |
BuiltInRuleInteractionFactory.register(java.lang.Class<T> clazz,
org.key_project.ui.interactionlog.model.builtin.Factory<T> factory) |
Copyright © 2003-2019 The KeY-Project.