Interface | Description |
---|---|
FinishSymbolicExecutionWithSpecJoinsMacro.Predicate<T> | |
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.
|
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
|
FinishSymbolicExecutionUntilJoinPointMacro |
The macro FinishSymbolicExecutionUntilJionPointMacro continues automatic rule
application until a join point is reached (i.e.
|
FinishSymbolicExecutionWithSpecJoinsMacro |
Finishes symbolic execution while taking JML join specifications into
account: Branches are joined at defined points during the execution.
|
FullAutoPilotProofMacro |
This class captures a proof macro which is meant to fully automise KeY proof
workflow.
|
FullAutoPilotWithJMLSpecJoinsProofMacro |
This class captures a proof macro which is meant to fully automate the 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.
|
OneStepProofMacro |
Apply a single proof step.
|
OneStepProofMacro.OneStepStrategy |
Strategy with counter, s.t.
|
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.
|
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.
|
WellDefinednessMacro.WellDefinednessStrategy |
This strategy accepts all rule apps for which the rule name is a
Well-Definedness rule and rejects everything else.
|