Package | Description |
---|---|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros |
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 | Class and Description |
---|---|
class |
AbstractBlastingMacro |
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.
|
Copyright © 2003-2019 The KeY-Project.