Package de.uka.ilkd.key.java.abstraction

This package contains the meta model abstractions as used by the semantical services.

See: Description

Interface Summary

Interface	Description
ArrayType	A program model element representing array types.
ClassType	A program model element representing class types.
ClassTypeContainer	A program model element that may contain class types.
Constructor	A program model element representing constructors.
Field	A program model element representing fields.
Member	A program model element representing members.
Method	A program model element representing methods.
ProgramModelElement	An entity of the program meta model.
Type	A program model element representing types.
Variable	A program model element representing variables.

Class Summary

Class	Description
DefaultConstructor	Deprecated is actually never used
KeYJavaType	The KeY java type realises a tuple (sort, type) of a logic sort and the java type (for example a class declaration).
KeYJavaType.LexicographicalKeYJavaTypeOrder<T extends KeYJavaType>
NullType	A program model element representing the null type.
Package	A program model element representing packages.
PrimitiveType	A program model element representing primitive types.

Package de.uka.ilkd.key.java.abstraction Description

This package contains the meta model abstractions as used by the semantical services. The ProgramModelElements hide the origin of the information, be it from Java source code, Java byte code, or predefined lacking any syntactical representation.

There are three implicitly defined entities - ArrayType, DefaultConstructor, and Package, as well as the predefined types NullType and the base class for the small number of PrimitiveTypes.

Scopes are attached to ScopeDefiningElements by SourceInfo implementations and should not be modified from others.