Interface | Description |
---|---|
StartSideProofMacro |
Class | Description |
---|---|
AbstractFinishAuxiliaryComputationMacro | |
AuxiliaryComputationAutoPilotMacro | |
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. |
FinishAuxiliaryBlockComputationMacro | |
FinishAuxiliaryComputationMacro | |
FinishAuxiliaryLoopComputationMacro | |
FinishAuxiliaryMethodComputationMacro | |
FullInformationFlowAutoPilotMacro | |
FullUseInformationFlowContractMacro | |
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.
|
StartAuxiliaryBlockComputationMacro | |
StartAuxiliaryComputationMacro | |
StartAuxiliaryLoopComputationMacro | |
StartAuxiliaryMethodComputationMacro | |
StateExpansionAndInfFlowContractApplicationMacro | |
UseInformationFlowContractMacro |
The macro UseInformationFlowContractMacro applies all applicable information
flow contracts.
|