public class InfFlowContractAppTacletExecutor extends RewriteTacletExecutor<InfFlowContractAppTaclet>
Modifier and Type | Field and Description |
---|---|
static Properties.Property<ImmutableList<Term>> |
INF_FLOW_CONTRACT_APPL_PROPERTY
Strategy property which saves the list of formulas which where added
by information flow contract applications.
|
taclet
Constructor and Description |
---|
InfFlowContractAppTacletExecutor(InfFlowContractAppTaclet taclet) |
Modifier and Type | Method and Description |
---|---|
protected void |
addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
private void |
updateStrategyInfo(Goal goal,
Term applFormula)
Add the contract application formula to the list of the
INF_FLOW_CONTRACT_APPL_PROPERTY.
|
applyAdd, applyReplacewith, getRewriteResult
apply
addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public static final Properties.Property<ImmutableList<Term>> INF_FLOW_CONTRACT_APPL_PROPERTY
public InfFlowContractAppTacletExecutor(InfFlowContractAppTaclet taclet)
protected void addToAntec(Semisequent semi, TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, SequentChangeInfo currentSequent, PosInOccurrence pos, PosInOccurrence applicationPosInOccurrence, MatchConditions matchCond, Goal goal, RuleApp tacletApp, Services services)
TacletExecutor
addToAntec
in class TacletExecutor<InfFlowContractAppTaclet>
semi
- the Semisequent with the the ConstrainedFormulae to be addedtermLabelState
- The TermLabelState
of the current rule application.labelHint
- The hint used to maintain TermLabel
s.currentSequent
- the Sequent which is the current (intermediate) result of applying the tacletpos
- the PosInOccurrence describing the place in the
sequent or null for head of antecedentapplicationPosInOccurrence
- The PosInOccurrence
of the Term
which is rewrittenmatchCond
- the MatchConditions containing in particular
the instantiations of the schemavariablesservices
- the Services encapsulating all java information