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.Services;
16: import de.uka.ilkd.key.java.TypeConverter;
17: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
18: import de.uka.ilkd.key.java.expression.Operator;
19: import de.uka.ilkd.key.java.reference.ExecutionContext;
20: import de.uka.ilkd.key.java.visitor.Visitor;
21: import de.uka.ilkd.key.util.ExtList;
22:
23: /**
24: * Binary not.
25: * @author <TT>AutoDoc</TT>
26: */
27:
28: public class BinaryNot extends Operator {
29:
30: /**
31: * Binary not.
32: * @param children list withh all children
33: */
34:
35: public BinaryNot(ExtList children) {
36: super (children);
37: }
38:
39: /**
40: * Get arity.
41: * @return the int value.
42: */
43:
44: public int getArity() {
45: return 1;
46: }
47:
48: /**
49: * Get precedence.
50: * @return the int value.
51: */
52:
53: public int getPrecedence() {
54: return 1;
55: }
56:
57: /**
58: * Get notation.
59: * @return the int value.
60: */
61:
62: public int getNotation() {
63: return PREFIX;
64: }
65:
66: /**
67: * Checks if this operator is left or right associative. Ordinary
68: * unary operators are right associative.
69: * @return <CODE>true</CODE>, if the operator is left associative,
70: * <CODE>false</CODE> otherwise.
71: */
72:
73: public boolean isLeftAssociative() {
74: return false;
75: }
76:
77: /** calls the corresponding method of a visitor in order to
78: * perform some action/transformation on this element
79: * @param v the Visitor
80: */
81: public void visit(Visitor v) {
82: v.performActionOnBinaryNot(this );
83: }
84:
85: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
86: p.printBinaryNot(this );
87: }
88:
89: public KeYJavaType getKeYJavaType(Services javaServ,
90: ExecutionContext ec) {
91: final TypeConverter tc = javaServ.getTypeConverter();
92: return tc.getPromotedType(tc.getKeYJavaType(
93: (Expression) getChildAt(0), ec));
94:
95: }
96: }
|