| java.lang.Object
 de.uka.ilkd.key.rule.TacletGoalTemplate
All known Subclasses: de.uka.ilkd.key.rule.RewriteTacletGoalTemplate, de.uka.ilkd.key.rule.AntecSuccTacletGoalTemplate,
| TacletGoalTemplate | | public class TacletGoalTemplate (Code) | | this class contains the goals of the schematic theory specific
rules (Taclet). There are new sequents that have to be added, new
rules and rule variables. The replacewith-goal is implemented in
subclasses
|
| TacletGoalTemplate | | public TacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules, SetOfSchemaVariable addedProgVars)(Code) | | creates new Goaldescription
Parameters:
addedSeq - new Sequent to be added
Parameters:
addedRules - ListOfTaclet contains the new allowed rulesat this branch
Parameters:
addedProgVars - a SetOfSchemaVariable which will be instantiated witha application time unused (new) program variables that are introduced by an application of this template |
| TacletGoalTemplate | | public TacletGoalTemplate(Sequent addedSeq, ListOfTaclet addedRules)(Code) | | creates new Goaldescription
same effect as new TacletGoalTemplate(addedSeq,
addedRules,
SetAsListOfSchemaVariable.EMPTY_SET)
Parameters:
addedSeq - new Sequent to be added
Parameters:
addedRules - ListOfTaclet contains the new allowed rulesat this branch |
| addedProgVars | | public SetOfSchemaVariable addedProgVars()(Code) | | returns the set of schemavaroable whos einstantiations will be
added to the sequent namespace
|
| getBoundVariables | | protected SetOfQuantifiableVariable getBoundVariables()(Code) | | rertieves and returns all variables that are bound in the
goal template
all variables that occur bound in this goal template |
| hashCode | | public int hashCode()(Code) | | |
| replaceWithExpressionAsObject | | Object replaceWithExpressionAsObject()(Code) | | a Taclet may replace parts of sequent.
term (or sequent) to be placed instead of the findexp-term.REMARK: returns 'null' if there is no replace-with part !Overwritten in subclasses ! |
| rules | | public ListOfTaclet rules()(Code) | | the goal of a Taclet may introduce new rules. Call this method
to get them
ListOfTaclet contains new introduced rules |
| sequent | | public Sequent sequent()(Code) | | a Taclet may add a new Sequent as Goal. Use this method to get
this Sequent
Sequent to be added as Goal or Sequent.EMPTY_SEQUENT ifno such Sequent exists |
|
|