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