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 |
Modifier and Type | Method and Description |
---|---|
ProofMacro |
ProofMacroApi.getMacro(java.lang.String name)
Searches for the proof script command in the registered commands by its name.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<ProofMacro> |
ProofMacroApi.getMacros()
Returns a collection of all registered proof script commands.
|
Modifier and Type | Method and Description |
---|---|
void |
DefaultProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
ProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
InteractionListener.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Modifier and Type | Field and Description |
---|---|
static java.lang.Iterable<ProofMacro> |
ProofMacroMenu.REGISTERED_MACROS
The loader used to access the providers for macros.
|
Modifier and Type | Method and Description |
---|---|
protected void |
ProofMacroWorker.emitProofMacroFinished(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Constructor and Description |
---|
ProofMacroWorker(Node node,
ProofMacro macro,
KeYMediator mediator,
PosInOccurrence posInOcc)
Instantiates a new proof macro worker.
|
Constructor and Description |
---|
MacroKeyBinding(KeYMediator mediator,
SequentView sequentView,
ProofMacro macro) |
Modifier and Type | Interface and Description |
---|---|
interface |
StartSideProofMacro |
Modifier and Type | Class and Description |
---|---|
class |
AbstractFinishAuxiliaryComputationMacro |
class |
AuxiliaryComputationAutoPilotMacro |
class |
ExhaustiveProofMacro
The abstract class ExhaustiveProofMacro can be used to create compound macros
which either apply the macro given by
ExhaustiveProofMacro.getProofMacro() directly, or
--if not directly applicable-- search on the sequent for any applicable
posInOcc and apply it on the first applicable one or --if not applicable
anywhere on the sequent-- do not apply it. |
class |
FinishAuxiliaryBlockComputationMacro |
class |
FinishAuxiliaryComputationMacro |
class |
FinishAuxiliaryLoopComputationMacro |
class |
FinishAuxiliaryMethodComputationMacro |
class |
FullInformationFlowAutoPilotMacro |
class |
FullUseInformationFlowContractMacro |
class |
SelfcompositionStateExpansionMacro
The macro SelfcompositionStateExpansionMacro applies rules to extract
the self-composed states after the merge of the symbolic execution goals
which is included in the proof obligation generation from information flow
contracts.
|
class |
StartAuxiliaryBlockComputationMacro |
class |
StartAuxiliaryComputationMacro |
class |
StartAuxiliaryLoopComputationMacro |
class |
StartAuxiliaryMethodComputationMacro |
class |
StateExpansionAndInfFlowContractApplicationMacro |
class |
UseInformationFlowContractMacro
The macro UseInformationFlowContractMacro applies all applicable information
flow contracts.
|
Modifier and Type | Method and Description |
---|---|
protected ProofMacro[] |
StartAuxiliaryComputationMacro.createProofMacroArray() |
protected ProofMacro[] |
StateExpansionAndInfFlowContractApplicationMacro.createProofMacroArray() |
protected ProofMacro[] |
FullUseInformationFlowContractMacro.createProofMacroArray() |
protected ProofMacro[] |
FinishAuxiliaryComputationMacro.createProofMacroArray() |
protected ProofMacro |
FullInformationFlowAutoPilotMacro.getAltProofMacro() |
protected ProofMacro |
FullInformationFlowAutoPilotMacro.getProofMacro() |
Modifier and Type | Class and Description |
---|---|
class |
AbstractBlastingMacro |
class |
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).
|
class |
AbstractPropositionalExpansionMacro
The Class AbstractPropositionalExpansionMacro applies purely propositional
rules.
|
class |
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.
|
class |
AutoMacro
The macro
AutoMacro is a customizable ProofMacro for use in
proof scripts. |
class |
AutoPilotPrepareProofMacro |
class |
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. |
class |
FinishSymbolicExecutionMacro
The macro FinishSymbolicExecutionMacro continues automatic rule application
until there is no more modality on the sequent.
|
class |
FinishSymbolicExecutionUntilMergePointMacro
The macro FinishSymbolicExecutionUntilJionPointMacro continues automatic rule
application until a merge point is reached (i.e.
|
class |
FullAutoPilotProofMacro
This class captures a proof macro which is meant to fully automise KeY proof
workflow.
|
class |
FullPropositionalExpansionMacro
The macro FullPropositionalExpansionMacro apply rules to decompose
propositional toplevel formulas; it even splits the goal if necessary.
|
class |
HeapSimplificationMacro
This macro performs simplification of Heap and LocSet terms.
|
class |
IntegerSimplificationMacro
This macro performs simplification of integers and terms with integers.
|
class |
OneStepProofMacro
Apply a single proof step.
|
class |
PrepareInfFlowContractPreBranchesMacro
The macro UseInformationFlowContractMacro applies all applicable information
flow contracts.
|
class |
PropositionalExpansionMacro
The macro PropositionalExpansionMacro apply rules to decompose propositional
toplevel formulas; but does not split the goal.
|
class |
PropositionalExpansionWithSimplificationMacro |
class |
SemanticsBlastingMacro |
class |
SequentialOnLastGoalProofMacro |
class |
SequentialProofMacro
The abstract class SequentialProofMacro can be used to create compound macros
which sequentially apply macros one after the other.
|
class |
SkipMacro
This macro does nothing and is not applicable.
|
class |
SMTPreparationMacro
A macro that performs all simplifications that are necessary in order to perform a translation
of the sequent to SMT.
|
class |
StrategyProofMacro
The abstract class StrategyProofMacro can be used to define proof macros
which use their own strategy.
|
class |
TestGenMacro |
class |
TryCloseMacro
The Class TryCloseMacro tries to close goals.
|
class |
UpdateSimplificationMacro
This macro applies only update simplification rules.
|
class |
WellDefinednessMacro
This macro resolves the well-definedness transformer, i.e.
|
Modifier and Type | Method and Description |
---|---|
protected ProofMacro[] |
FullAutoPilotProofMacro.createProofMacroArray() |
protected ProofMacro[] |
SMTPreparationMacro.createProofMacroArray()
Creates the proof macro array.
|
protected abstract ProofMacro[] |
SequentialProofMacro.createProofMacroArray()
Creates the proof macro array.
|
protected abstract ProofMacro[] |
AlternativeMacro.createProofMacroArray()
Creates the proof macro array.
|
protected abstract ProofMacro |
DoWhileFinallyMacro.getAltProofMacro()
Gets the alternative proof macro for the else-branch.
|
ProofMacro |
ProofMacroFinishedInfo.getMacro() |
protected abstract ProofMacro |
DoWhileFinallyMacro.getProofMacro()
Gets the proof macro.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<ProofMacro> |
SequentialProofMacro.getProofMacros()
Gets the proof macros.
|
java.util.List<ProofMacro> |
AlternativeMacro.getProofMacros()
Gets the proof macros.
|
Modifier and Type | Method and Description |
---|---|
static ProofMacroFinishedInfo |
ProofMacroFinishedInfo.getDefaultInfo(ProofMacro macro,
Proof proof) |
Constructor and Description |
---|
ProofMacroFinishedInfo(ProofMacro macro,
Goal goal) |
ProofMacroFinishedInfo(ProofMacro macro,
ImmutableList<Goal> goals) |
ProofMacroFinishedInfo(ProofMacro macro,
Proof proof) |
ProofMacroFinishedInfo(ProofMacro macro,
Proof proof,
boolean cancelled) |
ProofMacroFinishedInfo(ProofMacro macro,
ProofMacroFinishedInfo info) |
Modifier and Type | Method and Description |
---|---|
ProofMacro |
AbstractMediatorUserInterfaceControl.getMacro() |
Modifier and Type | Method and Description |
---|---|
void |
MediatorProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
AbstractMediatorUserInterfaceControl.setMacro(ProofMacro macro) |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Modifier and Type | Method and Description |
---|---|
void |
MacroInteraction.setMacro(ProofMacro macro) |
Constructor and Description |
---|
MacroInteraction(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Copyright © 2003-2019 The KeY-Project.