| java.lang.Object
 de.uka.ilkd.key.logic.Visitor
de.uka.ilkd.key.rule.TacletSchemaVariableCollector
All known Subclasses: de.uka.ilkd.key.rule.TacletVariableSVCollector,
| TacletSchemaVariableCollector | | public class TacletSchemaVariableCollector extends Visitor (Code) | | Collects all schemavariables occurring in the
\find, \assumes part or goal description of a taclet.
The addrule section is scanned optionally.
Duplicates are not removed because the use of persistent
datastructure and up to now we just have a SetAsList-implementaion
causing to have O(sqr(n)) if it would used.
For example,
de.uka.ilkd.key.rule.TacletApp uses this class
to determine all uninstantiated schemavariables.
|
| Field Summary | |
| protected ListOfSchemaVariable | varList
|
| varList | | protected ListOfSchemaVariable varList(Code) | | collects all found variables
|
| TacletSchemaVariableCollector | | public TacletSchemaVariableCollector()(Code) | | creates the Variable collector.
|
| TacletSchemaVariableCollector | | public TacletSchemaVariableCollector(SVInstantiations svInsts)(Code) | | creates the Variable collector.
Parameters:
svInsts - the SVInstantiations that have been already found(needed by unwind loop constructs to determine which labels are needed) |
| collectSVInProgram | | protected ListOfSchemaVariable collectSVInProgram(JavaBlock jb, ListOfSchemaVariable vars)(Code) | | collects all SchemVariables that occur in the JavaBlock
Parameters:
jb - the JavaBlock where to look for Schemavariables
Parameters:
vars - the ListOfSchemaVariable where to add the foundSchemaVariables the extended list of found schemavariables |
| size | | public int size()(Code) | | number of the found variables |
| varIterator | | public IteratorOfSchemaVariable varIterator()(Code) | | iterator of the found Variables |
| visit | | public void visit(Term t)(Code) | | visits the Term in post order
Term.execPostOrder(Visitor) and
collects all found schema variables
Parameters:
t - the Term whose schema variables are collected |
| visit | | public void visit(Sequent seq)(Code) | | goes through the given sequent an collects all vars found
Parameters:
seq - the Sequent to visit |
| visit | | public void visit(Taclet taclet, boolean visitAddrules)(Code) | | collects all schema variables of a taclet
Parameters:
taclet - the Taclet where the variables have to be collected to
Parameters:
visitAddrules - a boolean that contols if the addrule sections areto be ignored (iff false) or if the visitor descends into them (iff true) |
| visitFindPart | | protected void visitFindPart(Taclet taclet)(Code) | | |
| visitGoalTemplates | | protected void visitGoalTemplates(Taclet taclet, boolean visitAddrules)(Code) | | |
| visitWithoutAddrule | | public void visitWithoutAddrule(Taclet taclet)(Code) | | collects all variables in a Taclet but ignores the variables that appear
only in the addrule sections of the Taclet
Parameters:
taclet - the Taclet where the variables have to be collected to |
|
|