| 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.
|