de.uka.ilkd.key.java.expression

Class Assignment

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.java.expression.Operator

de.uka.ilkd.key.java.expression.Assignment

All Implemented Interfaces:

Expression, ExpressionStatement, ExpressionContainer, LoopInitializer, ModelElement, NonTerminalProgramElement, ProgramElement, SourceElement, Statement, SVSubstitute

Direct Known Subclasses:

BinaryAndAssignment, BinaryOrAssignment, BinaryXOrAssignment, CopyAssignment, DivideAssignment, MinusAssignment, ModuloAssignment, PlusAssignment, PostDecrement, PostIncrement, PreDecrement, PreIncrement, ShiftLeftAssignment, ShiftRightAssignment, TimesAssignment, UnsignedShiftRightAssignment

public abstract class Assignment
extends Operator
implements ExpressionStatement

An assignment is an operator with side-effects.

Field Summary

Fields inherited from class de.uka.ilkd.key.java.expression.Operator

children, INFIX, POSTFIX, PREFIX

Constructor Summary

Constructors

Constructor and Description
Assignment()
Assignment(Expression lhs) Unary Assignment (e.g. +=, ++).
Assignment(Expression lhs, Expression rhs) Assignment.
Assignment(ExtList children) Constructor for the transformation of COMPOST ASTs to KeY.

Method Summary

Modifier and Type	Method and Description
KeYJavaType	getKeYJavaType(Services javaServ, ExecutionContext ec) retrieves the type of the assignment expression
boolean	isLeftAssociative() Checks if this operator is left or right associative.
java.lang.String	reuseSignature(Services services, ExecutionContext ec) overriden from Operator

Methods inherited from class de.uka.ilkd.key.java.expression.Operator

getArguments, getArity, getChildAt, getChildCount, getExpressionAt, getExpressionCount, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getNotation, getPrecedence, isToBeParenthesized, precedes

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrint, prettyPrintMain

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Methods inherited from interface de.uka.ilkd.key.java.SourceElement

equalsModRenaming, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition, prettyPrint, visit

Constructor Detail

Assignment

public Assignment()

Assignment

public Assignment(ExtList children)

Constructor for the transformation of COMPOST ASTs to KeY.

Parameters:

children - the children of this AST element as KeY classes. In this case the order of the children is IMPORTANT. May contain: 2 of Expression (the first Expression as left hand side, the second as right hand side), Comments

Assignment

public Assignment(Expression lhs)

Unary Assignment (e.g. +=, ++).

Parameters:

lhs - an expression.

Assignment

public Assignment(Expression lhs,
                  Expression rhs)

Assignment.

Parameters:

lhs - an expression.

rhs - an expression.

Method Detail

isLeftAssociative

public boolean isLeftAssociative()

Checks if this operator is left or right associative. Assignments are right associative.

Overrides:

isLeftAssociative in class Operator

Returns:

true, if the operator is left associative, false otherwise.

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ,
                                  ExecutionContext ec)

retrieves the type of the assignment expression

Specified by:

getKeYJavaType in interface Expression

Specified by:

getKeYJavaType in class Operator

Parameters:

javaServ - the Services offering access to the Java model

ec - the ExecutionContext in which the expression is evaluated

Returns:

the type of the assignment expression

reuseSignature

public java.lang.String reuseSignature(Services services,
                                       ExecutionContext ec)

overriden from Operator

Overrides:

reuseSignature in class Operator

ec - TODO