de.uka.ilkd.key.informationflow.rule.executor

Class InfFlowContractAppTacletExecutor

java.lang.Object

de.uka.ilkd.key.rule.executor.javadl.TacletExecutor<TacletKind>

de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor<TacletKind>

de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor<InfFlowContractAppTaclet>

de.uka.ilkd.key.informationflow.rule.executor.InfFlowContractAppTacletExecutor

All Implemented Interfaces:

RuleExecutor

public class InfFlowContractAppTacletExecutor
extends RewriteTacletExecutor<InfFlowContractAppTaclet>

Field Summary

Fields

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.

Fields inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

taclet

Constructor Summary

Constructors

Constructor and Description
InfFlowContractAppTacletExecutor(InfFlowContractAppTaclet taclet)

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor

applyAdd, applyReplacewith, getRewriteResult

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor

apply

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

INF_FLOW_CONTRACT_APPL_PROPERTY

public static final 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. This list is used by the macros UseInformationFlowContractMacro and PrepareInfFlowContractPreBranchesMacro to decide how to prepare the formulas resulting from information flow contract applications.

Constructor Detail

InfFlowContractAppTacletExecutor

public InfFlowContractAppTacletExecutor(InfFlowContractAppTaclet taclet)

Method Detail

addToAntec

protected void addToAntec(Semisequent semi,
                          TermLabelState termLabelState,
                          Taclet.TacletLabelHint labelHint,
                          SequentChangeInfo currentSequent,
                          PosInOccurrence pos,
                          PosInOccurrence applicationPosInOccurrence,
                          MatchConditions matchCond,
                          Goal goal,
                          RuleApp tacletApp,
                          Services services)

Description copied from class: TacletExecutor

adds SequentFormula to antecedent depending on position information (if none is handed over it is added at the head of the antecedent). Of course it has to be ensured that the position information describes one occurrence in the antecedent of the sequent.

Overrides:

addToAntec in class TacletExecutor<InfFlowContractAppTaclet>

Parameters:

semi - the Semisequent with the the ConstrainedFormulae to be added

termLabelState - The TermLabelState of the current rule application.

labelHint - The hint used to maintain TermLabels.

currentSequent - the Sequent which is the current (intermediate) result of applying the taclet

pos - the PosInOccurrence describing the place in the sequent or null for head of antecedent

applicationPosInOccurrence - The PosInOccurrence of the Term which is rewritten

matchCond - the MatchConditions containing in particular the instantiations of the schemavariables

services - the Services encapsulating all java information

updateStrategyInfo

private void updateStrategyInfo(Goal goal,
                                Term applFormula)

Add the contract application formula to the list of the INF_FLOW_CONTRACT_APPL_PROPERTY.

Parameters:

goal - the current goal

applFormula - the information contract application formula added by this taclet