de.uka.ilkd.key.rule.tacletbuilder

Class SuccTacletBuilder

java.lang.Object

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

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

de.uka.ilkd.key.rule.tacletbuilder.SuccTacletBuilder

public class SuccTacletBuilder
extends FindTacletBuilder<SuccTaclet>

class builds SuccTaclet 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
private boolean	ignoreTopLevelUpdates

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
SuccTacletBuilder()

Method Summary

Modifier and Type	Method and Description
void	addTacletGoalTemplate(TacletGoalTemplate goal) adds a new goal descriptions to the goal descriptions of the Taclet.
SuccTaclet	getSuccTaclet() builds and returns the SuccTaclet that is specified by former set... / add... methods.
SuccTaclet	getTaclet() builds and returns the Taclet that is specified by former set... / add... methods.
SuccTacletBuilder	setFind(Term findTerm) sets the find of the Taclet that is to build to the given term, if the sort of the given term is of Sort.FORMULA otherwise nothing happens.
void	setIgnoreTopLevelUpdates(boolean ignore)

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

ignoreTopLevelUpdates

private boolean ignoreTopLevelUpdates

Constructor Detail

SuccTacletBuilder

public SuccTacletBuilder()

Method Detail

setFind

public SuccTacletBuilder setFind(Term findTerm)

sets the find of the Taclet that is to build to the given term, if the sort of the given term is of Sort.FORMULA otherwise nothing happens.

Returns:

this SuccTacletBuilder

addTacletGoalTemplate

public void addTacletGoalTemplate(TacletGoalTemplate goal)

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

Specified by:

addTacletGoalTemplate in class TacletBuilder<SuccTaclet>

getSuccTaclet

public SuccTaclet getSuccTaclet()

builds and returns the SuccTaclet 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 semisequents. No specification for the interactive or recursive flags imply that the flags are not set. No specified find part causes an IllegalStateException. 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.

getTaclet

public SuccTaclet 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<SuccTaclet>

setIgnoreTopLevelUpdates

public void setIgnoreTopLevelUpdates(boolean ignore)