de.uka.ilkd.key.rule.tacletbuilder

Class RewriteTacletBuilder<T extends RewriteTaclet>

java.lang.Object

de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder<T>

de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder<T>

de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder<T>

Direct Known Subclasses:

AbstractInfFlowContractAppTacletBuilder.InfFlowContractAppRewriteTacletBuilder

public class RewriteTacletBuilder<T extends RewriteTaclet>
extends FindTacletBuilder<T>

class builds RewriteTaclet objects.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

TacletBuilder.TacletBuilderException

Field Summary

Fields

Modifier and Type	Field and Description
protected int	applicationRestriction encodes restrictions on the state where a rewrite taclet is applicable If the value is equal to RewriteTaclet.NONE no state restrictions are posed RewriteTaclet.SAME_UPDATE_LEVEL then \assumes must match on a formula within the same state as \find rsp.
protected boolean	surviveSmbExec

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder

find

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn

Constructor Summary

Constructors

Constructor and Description
RewriteTacletBuilder()

Method Summary

Modifier and Type	Method and Description
void	addGoalTerm(Term goalTerm)
void	addTacletGoalTemplate(TacletGoalTemplate goal) adds a new goal descriptions to the goal descriptions of the Taclet.
T	getRewriteTaclet() builds and returns the RewriteTaclet that is specified by former set... / add... methods.
T	getTaclet() builds and returns the Taclet that is specified by former set... / add... methods.
RewriteTacletBuilder<T>	setApplicationRestriction(int p_applicationRestriction)
RewriteTacletBuilder<T>	setFind(Term findTerm) sets the find of the Taclet that is to build to the given term.
void	setSurviveSmbExec(boolean b)

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder

checkBoundInIfAndFind, getFind

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

addGoal2ChoicesMapping, addRuleSet, addVariableCondition, addVarsNew, addVarsNew, addVarsNew, addVarsNew, addVarsNewDependingOn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, checkContainsFreeVarSV, checkContainsFreeVarSV, getChoices, getGoal2Choices, getName, getTacletWithoutInactiveGoalTemplates, goalTemplates, ifSequent, setAnnotations, setChoices, setDisplayName, setHelpText, setIfSequent, setName, setRuleSets, setTacletGoalTemplates, setTrigger, varsNotFreeIn

Methods inherited from class java.lang.Object

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

Field Detail

applicationRestriction

protected int applicationRestriction

encodes restrictions on the state where a rewrite taclet is applicable If the value is equal to

• RewriteTaclet.NONE no state restrictions are posed
• RewriteTaclet.SAME_UPDATE_LEVEL then \assumes must match on a formula within the same state as \find rsp. \add. For efficiency no modalities are allowed above the \find position
• RewriteTaclet.IN_SEQUENT_STATE the \find part is only allowed to match on formulas which are evaluated in the same state as the sequent

surviveSmbExec

protected boolean surviveSmbExec

Constructor Detail

RewriteTacletBuilder

public RewriteTacletBuilder()

Method Detail

setApplicationRestriction

public RewriteTacletBuilder<T> setApplicationRestriction(int p_applicationRestriction)

setSurviveSmbExec

public void setSurviveSmbExec(boolean b)

setFind

public RewriteTacletBuilder<T> setFind(Term findTerm)

sets the find of the Taclet that is to build to the given term.

Returns:

this RewriteTacletBuilder

getRewriteTaclet

public T getRewriteTaclet()

builds and returns the RewriteTaclet that is specified by former set... / add... methods. If no name is specified then an Taclet with an empty string name is build. No specifications for variable conditions, goals or heuristics imply that the corresponding parts of the Taclet are empty. No specification for the if-sequent is represented as a sequent with two empty semisequents. No specification for the interactive or recursive flags imply that the flags are not set. No specified find part causes an TacletBuilderException. Throws an TacletBuilderException if a bound SchemaVariable occurs more than once in if and find or an InvalidPrefixException if the building of the Taclet Prefix fails.

addTacletGoalTemplate

public void addTacletGoalTemplate(TacletGoalTemplate goal)

adds a new goal descriptions to the goal descriptions of the Taclet. the TacletGoalTemplate must not be an AntecSuccTacletGoalTemplate, otherwise an illegal argument exception is thrown.

Specified by:

addTacletGoalTemplate in class TacletBuilder<T extends RewriteTaclet>

addGoalTerm

public void addGoalTerm(Term goalTerm)

getTaclet

public T getTaclet()

builds and returns the Taclet that is specified by former set... / add... methods. If no name is specified then an Taclet with an empty string name is build. No specifications for variable conditions, goals or heuristics imply that the corresponding parts of the Taclet are empty. No specification for the if-sequence is represented as a sequent with two empty semisequences. No specification for the interactive or recursive flags imply that the flags are not set. No specified find part causes an IllegalStateException.

Specified by:

getTaclet in class TacletBuilder<T extends RewriteTaclet>