01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.rule;
12:
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16:
17: /** This class is used to collect all appearing SchemaVariables that are bound in a
18: * Taclet. Duplicates are not removed becaues the use of persistent
19: * datastructure and up to now we just have a SetAsList-implementaion
20: * causing to have O(sqr(n)) if it would used.
21: * The class is used by RuleApps to compute all non-instantiated variables.
22: */
23: public class TacletVariableSVCollector extends
24: TacletSchemaVariableCollector {
25:
26: /**
27: * visits term t in post order
28: * ({@link Term#execPostOrder(de.uka.ilkd.key.logic.Visitor)})
29: * and collects all bound schema variables
30: * @param t the Term to be visited (<code>t</code> must not be <code>null</code>
31: */
32: public void visit(Term t) {
33: for (int j = 0; j < t.arity(); j++) {
34: for (int i = 0; i < t.varsBoundHere(j).size(); i++) {
35: QuantifiableVariable boundVar = t.varsBoundHere(j)
36: .getQuantifiableVariable(i);
37: if (boundVar instanceof SchemaVariable) {
38: varList = varList
39: .prepend((SchemaVariable) boundVar);
40: }
41: }
42: }
43: }
44:
45: }
|