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.java.expression.operator;
12:
13: import de.uka.ilkd.key.java.Expression;
14: import de.uka.ilkd.key.java.PrettyPrinter;
15: import de.uka.ilkd.key.java.visitor.Visitor;
16: import de.uka.ilkd.key.util.ExtList;
17:
18: /**
19: * Times.
20: * @author <TT>AutoDoc</TT>
21: */
22:
23: public class Times extends BinaryOperator {
24:
25: /**
26: * Times.
27: * @param lhs an expression.
28: * @param rhs an expression.
29: */
30:
31: public Times(Expression lhs, Expression rhs) {
32: super (lhs, rhs);
33: }
34:
35: /**
36: * Constructor for the transformation of COMPOST ASTs to KeY.
37: * The first occurrence of an Expression in the given list is taken as
38: * the left hand side
39: * of the expression, the second occurrence is taken as the right hand
40: * side of the expression.
41: * @param children the children of this AST element as KeY classes.
42: */
43: public Times(ExtList children) {
44: super (children);
45: }
46:
47: /**
48: * Get precedence.
49: * @return the int value.
50: */
51:
52: public int getPrecedence() {
53: return 2;
54: }
55:
56: /**
57: * Get notation.
58: * @return the int value.
59: */
60:
61: public int getNotation() {
62: return INFIX;
63: }
64:
65: /** calls the corresponding method of a visitor in order to
66: * perform some action/transformation on this element
67: * @param v the Visitor
68: */
69: public void visit(Visitor v) {
70: v.performActionOnTimes(this );
71: }
72:
73: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
74: p.printTimes(this);
75: }
76:
77: }
|