de.uka.ilkd.key.java

Interface Expression

All Superinterfaces:

ModelElement, ProgramElement, SourceElement, SVSubstitute

All Known Subinterfaces:

ExpressionStatement, ProgramConstruct

All Known Implementing Classes:

AbstractIntegerLiteral, AllFields, AllObjects, ArrayInitializer, ArrayLength, ArrayLengthReference, ArrayPostDecl, ArrayReference, Assignment, BinaryAnd, BinaryAndAssignment, BinaryNot, BinaryOperator, BinaryOr, BinaryOrAssignment, BinaryXOr, BinaryXOrAssignment, BooleanLiteral, CharLiteral, ComparativeOperator, Conditional, ConstructorCall, CopyAssignment, CreateObject, Divide, DivideAssignment, DLEmbeddedExpression, DoBreak, DoubleLiteral, EmptyMapLiteral, EmptySeqLiteral, EmptySetLiteral, EnhancedForElimination, Equals, EvaluateArgs, ExactInstanceof, ExpandMethodBody, FieldReference, FloatLiteral, ForInitUnfoldTransformer, ForToWhile, FreeLiteral, GreaterOrEquals, GreaterThan, InitArray, InitArrayCreation, Instanceof, Intersect, IntLiteral, IsStatic, LessOrEquals, LessThan, Literal, LocationVariable, LogicalAnd, LogicalNot, LogicalOr, LongLiteral, MetaClassReference, MethodCall, MethodReference, Minus, MinusAssignment, Modulo, ModuloAssignment, MultipleVarDecl, Negative, New, NewArray, NotEquals, NullLiteral, Operator, ParenthesizedExpression, PassiveExpression, Plus, PlusAssignment, Positive, PostDecrement, PostIncrement, PostWork, PreDecrement, PreIncrement, ProgramConstant, ProgramSV, ProgramTransformer, ProgramVariable, RealLiteral, SchematicFieldReference, SeqConcat, SeqGet, SeqIndexOf, SeqLength, SeqReverse, SeqSingleton, SeqSub, SetMinus, SetUnion, ShiftLeft, ShiftLeftAssignment, ShiftRight, ShiftRightAssignment, Singleton, SpecialConstructorCall, StaticInitialisation, StringLiteral, SuperReference, SwitchToIf, ThisReference, Times, TimesAssignment, TypeCast, TypeOf, TypeOperator, Unpack, UnsignedShiftRight, UnsignedShiftRightAssignment, UnwindLoop, VariableReference

public interface Expression
extends ProgramElement

Expression taken from COMPOST and changed to achieve an immutable structure

Method Summary

Modifier and Type	Method and Description
KeYJavaType	getKeYJavaType(Services javaServ, ExecutionContext ec) returns the KeYJavaType of an expression

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

Method Detail

getKeYJavaType

KeYJavaType getKeYJavaType(Services javaServ,
                           ExecutionContext ec)

returns the KeYJavaType of an expression