001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java.expression;
012:
013: import de.uka.ilkd.key.java.Expression;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
017: import de.uka.ilkd.key.java.reference.ExecutionContext;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /**
021: * An assignment is an operator with side-effects.
022: */
023:
024: public abstract class Assignment extends Operator implements
025: ExpressionStatement {
026:
027: public Assignment() {
028:
029: }
030:
031: /**
032: * Constructor for the transformation of COMPOST ASTs to KeY.
033: * @param children the children of this AST element as KeY classes.
034: * In this case the order of the children is IMPORTANT.
035: * May contain:
036: * 2 of Expression (the first Expression as left hand
037: * side, the second as right hand side),
038: * Comments
039: */
040: public Assignment(ExtList children) {
041: super (children);
042: }
043:
044: /**
045: Unary Assignment (e.g. +=, ++).
046: @param lhs an expression.
047: */
048: public Assignment(Expression lhs) {
049: super (lhs);
050: }
051:
052: /**
053: Assignment.
054: @param lhs an expression.
055: @param rhs an expression.
056: */
057: public Assignment(Expression lhs, Expression rhs) {
058: super (lhs, rhs);
059: }
060:
061: /**
062: * Checks if this operator is left or right associative. Assignments
063: * are right associative.
064: * @return <CODE>true</CODE>, if the operator is left associative,
065: * <CODE>false</CODE> otherwise.
066: */
067:
068: public boolean isLeftAssociative() {
069: return false;
070: }
071:
072: /**
073: * retrieves the type of the assignment expression
074: * @param javaServ the Services offering access to the Java model
075: * @param ec the ExecutionContext in which the expression is evaluated
076: * @return the type of the assignment expression
077: */
078: public KeYJavaType getKeYJavaType(Services javaServ,
079: ExecutionContext ec) {
080: return getExpressionAt(0).getKeYJavaType(javaServ, ec);
081: }
082:
083: /** overriden from Operator
084: */
085: public String reuseSignature(Services services, ExecutionContext ec) {
086: String base = super .reuseSignature(services, ec);
087: Expression rhs;
088: try {
089: rhs = children.getExpression(1);
090: } catch (ArrayIndexOutOfBoundsException e) {
091: // no second argument, e.g. PostIncrement
092: return base;
093: }
094: if (rhs instanceof BooleanLiteral)
095: return base + "[" + rhs + "]";
096: else
097: return base;
098: }
099:
100: }
|