public class FinishAuxiliaryBlockComputationMacro extends AbstractFinishAuxiliaryComputationMacro
ProofMacro.ProgressBarListener
Constructor and Description |
---|
FinishAuxiliaryBlockComputationMacro() |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
private Taclet |
buildBlockInfFlowUnfoldTaclet(Services services,
BlockContractInternalBuiltInRuleApp blockRuleApp,
BlockContract contract,
IFProofObligationVars ifVars,
Term result)
constructs a taclet to unfold block contracts for information flow reasoning
|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
|
addContractApplicationTaclets, calculateResultingTerm, getCategory, getDescription, getName
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
public FinishAuxiliaryBlockComputationMacro()
public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
ProofMacro
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedpublic ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener)
ProofMacro
InterruptedException
.
A ProverTaskListener
can be provided to which the progress will
be reported. If no reports are desired, null
cna be used for
this parameter. If more than one listener is needed, consider combining
them using a single listener object using the composite pattern.uic
- the UserInterfaceControl
to useproof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)listener
- the listener to use for progress reports (may be
null
)private Taclet buildBlockInfFlowUnfoldTaclet(Services services, BlockContractInternalBuiltInRuleApp blockRuleApp, BlockContract contract, IFProofObligationVars ifVars, Term result)
services
- the ServicesblockRuleApp
- the rule application of the block contractcontract
- the block contractifVars
- variables specific for the IF proof obligationresult
- the term representing the result (?) // TODO: someone who knows what the taclet does please provide a description