Interface | Description |
---|---|
ProofMacro |
The interface ProofMacro is the entry point to a general strategy extension
system.
|
Class | 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.
|
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.
|
AutoMacro |
The macro
AutoMacro is a customizable ProofMacro for use in
proof scripts. |
AutoMacro.AutoMacroFilterStrategy |
The Class FilterAppManager is a special strategy assigning to any rule
infinite costs if the goal has no modality
|
AutoPilotPrepareProofMacro | |
AutoPilotPrepareProofMacro.AutoPilotStrategy | |
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. |
FilterStrategy | |
FinishSymbolicExecutionMacro |
The macro FinishSymbolicExecutionMacro continues automatic rule application
until there is no more modality on the sequent.
|
FinishSymbolicExecutionMacro.FilterSymbexStrategy |
The Class FilterAppManager is a special strategy assigning to any rule
infinite costs if the goal has no modality
|
FinishSymbolicExecutionUntilMergePointMacro |
The macro FinishSymbolicExecutionUntilJionPointMacro continues automatic rule
application until a merge point is reached (i.e. a point where a
MergeRule can
be applied) or there is no more modality on the sequent. |
FullAutoPilotProofMacro |
This class captures a proof macro which is meant to fully automise KeY proof
workflow.
|
FullPropositionalExpansionMacro |
The macro FullPropositionalExpansionMacro apply rules to decompose
propositional toplevel formulas; it even splits the goal if necessary.
|
HeapSimplificationMacro |
This macro performs simplification of Heap and LocSet terms.
|
IntegerSimplificationMacro |
This macro performs simplification of integers and terms with integers.
|
OneStepProofMacro |
Apply a single proof step.
|
OneStepProofMacro.OneStepStrategy |
Strategy with counter, s.t. only one rule is applied
|
PrepareInfFlowContractPreBranchesMacro |
The macro UseInformationFlowContractMacro applies all applicable information
flow contracts.
|
ProofMacro.ProgressBarListener |
This observer acts as intermediate instance between the reports by the
strategy and the UI reporting progress.
|
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).
|
PropositionalExpansionMacro |
The macro PropositionalExpansionMacro apply rules to decompose propositional
toplevel formulas; but does not split the goal.
|
PropositionalExpansionWithSimplificationMacro | |
SemanticsBlastingMacro | |
SequentialOnLastGoalProofMacro | |
SequentialProofMacro |
The abstract class SequentialProofMacro can be used to create compound macros
which sequentially apply macros one after the other.
|
SkipMacro |
This macro does nothing and is not applicable.
|
SMTPreparationMacro |
A macro that performs all simplifications that are necessary in order to perform a translation
of the sequent to SMT.
|
StrategyProofMacro |
The abstract class StrategyProofMacro can be used to define proof macros
which use their own strategy.
|
TestGenMacro | |
TestGenMacro.TestGenStrategy |
The Class FilterAppManager is a special strategy assigning to any rule
infinite costs if the goal has no modality
|
TryCloseMacro |
The Class TryCloseMacro tries to close goals.
|
TryCloseMacro.TryCloseProgressBarListener | |
UpdateSimplificationMacro |
This macro applies only update simplification rules.
|
WellDefinednessMacro |
This macro resolves the well-definedness transformer, i.e. it applies exactly
all applicable rules to resolve the operators WD and wd (which are formula/term
transformers).
|
WellDefinednessMacro.WellDefinednessStrategy |
This strategy accepts all rule apps for which the rule name is a
Well-Definedness rule and rejects everything else.
|