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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
11: // and Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16:
17: package de.uka.ilkd.key.logic;
18:
19: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
20:
21: /**
22: * A TermWithBoundVars is an object that contains a Term and 0, 1,
23: * or 2 QuantifiableVariable that are bound in the Term.
24: * This class is needed for OCL simplification when parsing the
25: * arguments of an OCL Collection operation.
26: */
27: public class TermWithBoundVars {
28:
29: /**
30: * the variables that are bound in the Term
31: */
32: public ArrayOfQuantifiableVariable boundVars;
33:
34: /**
35: * the Term
36: */
37: public Term term;
38:
39: /** creates a term with (possibly) bound variables
40: * @param vars the variables that are bound in t
41: * @param t the term
42: */
43: public TermWithBoundVars(ArrayOfQuantifiableVariable vars, Term t) {
44: boundVars = vars;
45: term = t;
46: }
47:
48: }
|