| java.lang.Object
 de.uka.ilkd.key.rule.TacletBuilder
de.uka.ilkd.key.rule.NoFindTacletBuilder
| NoFindTacletBuilder | | public class NoFindTacletBuilder extends TacletBuilder (Code) | | Due to the immutability of
Taclet s, they are created in the parsers
using
TacletBuilder s. This builder is used for
NoFindTaclet rules. Besides this some tests are performed that avoid
some common errors on applicability of taclets.
|
| addTacletGoalTemplate | | public void addTacletGoalTemplate(TacletGoalTemplate goal)(Code) | | adds a new goal descriptions to the goal descriptions of the Taclet.
Parameters:
goal - the TacletGoalTemplate specifying all the changes to be madeto achieve one of the resulting goals |
| checkBoundInIfAndFind | | protected void checkBoundInIfAndFind()(Code) | | checks that a variableSV occurrs at most once in a quantifier of the
ifs and finds and throws an exception otherwise
|
| getNoFindTaclet | | public NoFindTaclet getNoFindTaclet()(Code) | | 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
semisequences. No specification for the interactive or
recursive flags imply that the flags are not set.
|
| getTaclet | | public Taclet getTaclet()(Code) | | 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-sequent is represented as a sequent with two empty
semisequences. No specification for the interactive or
recursive flags imply that the flags are not set. May throw an
TacletBuilderException if a bound SchemaVariable occurs more than once in if
and find.
|
| Methods inherited from de.uka.ilkd.key.rule.TacletBuilder | public void addGoal2ChoicesMapping(TacletGoalTemplate gt, SetOfChoice soc)(Code)(Java Doc)
public void addOldName(String s)(Code)(Java Doc)
public void addRuleSet(RuleSet rs)(Code)(Java Doc)
abstract public void addTacletGoalTemplate(TacletGoalTemplate goal)(Code)(Java Doc)
public void addVariableCondition(VariableCondition vc)(Code)(Java Doc)
public void addVarsNew(SchemaVariable v, SchemaVariable asSort, boolean elementsort)(Code)(Java Doc)
public void addVarsNew(SchemaVariable v, SchemaVariable asSort)(Code)(Java Doc)
public void addVarsNew(SchemaVariable v, Sort sort)(Code)(Java Doc)
public void addVarsNew(NewVarcond nv)(Code)(Java Doc)
public void addVarsNew(ListOfNewVarcond list)(Code)(Java Doc)
public void addVarsNewDependingOn(SchemaVariable v0, SchemaVariable v1)(Code)(Java Doc)
public void addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1)(Code)(Java Doc)
public void addVarsNotFreeIn(ListOfNotFreeIn list)(Code)(Java Doc)
static void checkContainsFreeVarSV(Sequent seq, Name tacletName, String str)(Code)(Java Doc)
static void checkContainsFreeVarSV(Term t, Name tacletName, String str)(Code)(Java Doc)
public SetOfChoice getChoices()(Code)(Java Doc)
public HashMap getGoal2Choices()(Code)(Java Doc)
public Name getName()(Code)(Java Doc)
abstract public Taclet getTaclet()(Code)(Java Doc)
public Taclet getTacletWithoutInactiveGoalTemplates(SetOfChoice active)(Code)(Java Doc)
public ListOfTacletGoalTemplate goalTemplates()(Code)(Java Doc)
public Sequent ifSequent()(Code)(Java Doc)
public void setChoices(SetOfChoice choices)(Code)(Java Doc)
public void setConstraint(Constraint constraint)(Code)(Java Doc)
public void setDisplayName(String s)(Code)(Java Doc)
public void setHelpText(String s)(Code)(Java Doc)
public void setIfSequent(Sequent seq)(Code)(Java Doc)
public void setName(Name name)(Code)(Java Doc)
public void setNoninteractive(boolean ni)(Code)(Java Doc)
public void setRuleSets(ListOfRuleSet rs)(Code)(Java Doc)
public void setTacletGoalTemplates(ListOfTacletGoalTemplate g)(Code)(Java Doc)
public IteratorOfNotFreeIn varsNotFreeIn()(Code)(Java Doc)
|
|
|