Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
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.actions | |
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.ui | |
org.key_project.ui.interactionlog | |
org.key_project.ui.interactionlog.model |
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
Class and Description |
---|
AbstractProofMacro
Takes care of providing the whole ProofMacro interface by only making it
necessary to implement to most general application methods for a given
list of goals and translating the less general versions (firstly for a
given node and secondly having neither any goals nor a node).
|
AbstractPropositionalExpansionMacro
The Class AbstractPropositionalExpansionMacro applies purely propositional
rules.
|
AlternativeMacro
The abstract class AlternativeMacro can be used to create compound macros
which apply the first applicable macro (similar to a shortcut disjunction)
and then it returns.
|
DoWhileFinallyMacro
The abstract class DoWhileFinallyMacro can be used to create compound macros
which apply the macro given by
DoWhileFinallyMacro.getProofMacro() as long the given bound
of steps is not reached yet, the condition given by DoWhileFinallyMacro.getCondition()
holds, and the macro is applicable. |
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
SequentialProofMacro
The abstract class SequentialProofMacro can be used to create compound macros
which sequentially apply macros one after the other.
|
StrategyProofMacro
The abstract class StrategyProofMacro can be used to define proof macros
which use their own strategy.
|
Class and Description |
---|
AbstractBlastingMacro |
AbstractProofMacro
Takes care of providing the whole ProofMacro interface by only making it
necessary to implement to most general application methods for a given
list of goals and translating the less general versions (firstly for a
given node and secondly having neither any goals nor a node).
|
AbstractPropositionalExpansionMacro
The Class AbstractPropositionalExpansionMacro applies purely propositional
rules.
|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
ProofMacroListener
Listener for the application of proof macros (which may be run in
a separate worker thread).
|
SequentialProofMacro
The abstract class SequentialProofMacro can be used to create compound macros
which sequentially apply macros one after the other.
|
StrategyProofMacro
The abstract class StrategyProofMacro can be used to define proof macros
which use their own strategy.
|
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
Class and Description |
---|
ProofMacro
The interface ProofMacro is the entry point to a general strategy extension
system.
|
ProofMacroFinishedInfo
An information object with additional information about the
finished proof macro.
|
Copyright © 2003-2019 The KeY-Project.