Renovation: package.html to package-info.java

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java

@@ -0,0 +1,8 @@
+/**
+ * RIFL is short for "Requirements for Information Flow Language",
+ * a tool-indepentent specification language developed in the RS3 project.
+ * The RIFL/Java dialect is documented in XXX.
+ * This package contains a transformer from input RIFL files (XML) and
+ * original Java files to JML* annotated files.
+ */
+package de.uka.ilkd.key.util.rifl;

key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java

@@ -0,0 +1,19 @@
+/**
+ * This package contains the metamodel abstractions as used by the
+ * semantical services. The {@link recoder.abstraction.ProgramModelElement}s
+ * hide the origin of the information, be it from Java source code,
+ * Java byte code, or predefined lacking any syntactical representation.
+ * <p>
+ * There are three implicitly defined entities -
+ * {@link recoder.abstraction.ArrayType},
+ * {@link recoder.abstraction.DefaultConstructor}, and
+ * {@link recoder.abstraction.Package}, as well as the predefined
+ * types {@link recoder.abstraction.NullType} and the base class for
+ * the small number of {@link recoder.abstraction.PrimitiveType}s.
+ * <p>
+ * {@link recoder.abstraction.Scope}s are attached to
+ * {@link recoder.abstraction.ScopeDefiningElement}s by
+ * {@link recoder.service.SourceInfo} implementations and should
+ * not be modified from others.
+ */
+package de.uka.ilkd.key.java.abstraction;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java

@@ -0,0 +1,6 @@
+/**
+ * This package collects all Java modifiers. The sole abstraction beneath
+ * the parent {@link recoder.java.declaration.Modifier} is the
+ * {@link recoder.java.declaration.modifier.VisibilityModifier}.
+ */
+package de.uka.ilkd.key.java.declaration.modifier;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java

@@ -0,0 +1,11 @@
+/**
+ * Elements of the Java syntax tree representing declarations.
+ * For each declaration, there exists a corresponding
+ * {@link recoder.java.Reference} in the {@link recoder.java.reference}
+ * package.
+ * Each {@link recoder.java.Declaration}
+ * provides some convenience methods that query the possible modifiers.
+ * The modifiers themselves are collected in the subpackage
+ * {@link recoder.java.declaration.modifier}.
+ */
+package de.uka.ilkd.key.java.declaration;

key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java

@@ -0,0 +1,7 @@
+/**
+ * This package contains representations for the various Java literal types.
+ * Quite special are the non-primitive
+ * {@link recoder.java.expression.literal.NullLiteral} and
+ * {@link recoder.java.expression.literal.StringLiteral}.
+ */
+package de.uka.ilkd.key.java.expression.literal;

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java

@@ -0,0 +1,7 @@
+/**
+ * Elements of the Java syntax tree representing operators and operator-like
+ * expressions.
+ * {@link recoder.java.expression.operator.New} is also considered an
+ * operator ({@link recoder.java.expression.operator.TypeOperator}).
+ */
+package de.uka.ilkd.key.java.expression.operator;

key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java

@@ -0,0 +1,6 @@
+/**
+ * Elements of the Java syntax tree representing expressions.
+ * The various operators and literals are bundled in the corresponding
+ * subpackages.
+ */
+package de.uka.ilkd.key.java.expression;

key.core/src/main/java/de/uka/ilkd/key/java/package-info.java

@@ -0,0 +1,105 @@
+/**
+ * This package contains classes that cover the Java programming language.
+ * The classes in the subpackages are mainly taken from the Recoder
+ * framework and made immutable. They are transformed into this data
+ * structure from a Recoder structure by {@link
+ * de.uka.ilkd.key.java.Recoder2KeY} or {@link
+ * de.uka.ilkd.key.SchemaRecoder2KeY}. However, in some details both
+ * data structures might differ more.
+ * The following explanations are adapted from the
+ * documentation of the Recoder framework.
+ * <DL>
+ * <DT>Source and Program Elements</DT>
+ * <DD>
+ * A {@link de.uka.ilkd.key.java.SourceElement} is a syntactical entity and not
+ * necessary a {@link de.uka.ilkd.key.java.ModelElement}, such as a
+ * {@link de.uka.ilkd.key.java.Comment}.
+ * <p>
+ * A {@link de.uka.ilkd.key.java.ProgramElement} is a {@link de.uka.ilkd.key.java.SourceElement}
+ * and a {@link de.uka.ilkd.key.ModelElement}. It is aware of its parent in the syntax
+ * tree, while a pure {@link de.uka.ilkd.key.java.SourceElement} is not considered as a
+ * member of the AST even though it is represented in the sources.
+ * <p>
+ * {@link de.uka.ilkd.key.java.ProgramElement}s are further
+ * classified into {@link de.uka.ilkd.key.java.TerminalProgramElement}s and
+ * {@link de.uka.ilkd.key.java.NonTerminalProgramElement}s. While
+ * {@link de.uka.ilkd.key.java.TerminalProgramElement}
+ * is just a tag class, {@link de.uka.ilkd.key.java.NonTerminalProgramElement}s know
+ * their AST children (while it is possible that they do not have any).
+ * A complete source file occurs as a {@link de.uka.ilkd.key.java.CompilationUnit}.
+ * <p>
+ * {@link de.uka.ilkd.key.java.JavaSourceElement} and
+ * {@link de.uka.ilkd.key.java.JavaProgramElement} are abstract classes defining
+ * standard implementations that already know their
+ * {@link de.uka.ilkd.key.java.JavaProgramFactory}.
+ * </DD>
+ * <p>
+ * <DT>Expressions and Statements</DT>
+ * <DD>
+ * {@link de.uka.ilkd.key.java.Expression} and {@link de.uka.ilkd.key.java.Statement} are
+ * self-explanatory. A {@link de.uka.ilkd.key.java.LoopInitializer} is a special
+ * {@link de.uka.ilkd.key.java.Statement} valid as initializer of
+ * {@link de.uka.ilkd.key.java.statement.For} loops.
+ * {@link de.uka.ilkd.key.java.LoopInitializer} is subtyped by
+ * {@link de.uka.ilkd.key.java.expression.ExpressionStatement} and
+ * {@link de.uka.ilkd.key.java.declaration.LocalVariableDeclaration}).
+ * <p>
+ * Concrete classes and further abstractions are bundled in the
+ * {@link de.uka.ilkd.key.java.expression} and {@link de.uka.ilkd.key.java.statement} packages.
+ * </DD>
+ * <p>
+ * <DT>Syntax Tree Parents</DT>
+ * <DD>
+ * There are a couple of abstractions dealing with properties of being a
+ * parent node.
+ * <p>
+ * These are {@link de.uka.ilkd.key.java.declaration.TypeDeclarationContainer},
+ * {@link de.uka.ilkd.key.java.ExpressionContainer},
+ * {@link de.uka.ilkd.key.java.StatementContainer},
+ * {@link de.uka.ilkd.key.java.ParameterContainer},
+ * {@link de.uka.ilkd.key.java.NamedProgramElement} and
+ * {@link de.uka.ilkd.key.java.reference.TypeReferenceContainer}. A
+ * An {@link de.uka.ilkd.key.java.ExpressionContainer} contains
+ * {@link de.uka.ilkd.key.java.Expression}s, a
+ * {@link de.uka.ilkd.key.java.StatementContainer} contains
+ * {@link de.uka.ilkd.key.java.Statement}s, a
+ * {@link de.uka.ilkd.key.java.ParameterContainer}
+ * (either a {@link de.uka.ilkd.key.java.declaration.MethodDeclaration} or a
+ * {@link de.uka.ilkd.key.java.statement.Catch} statement) contains
+ * {@link de.uka.ilkd.key.java.declaration.ParameterDeclaration}s.
+ * A {@link de.uka.ilkd.key.java.NamedProgramElement} is a subtype of
+ * {@link de.uka.ilkd.key.java.NamedModelElement}.
+ * A {@link de.uka.ilkd.key.java.reference.TypeReferenceContainer} contains one or
+ * several names, but these are names of types that are referred to explicitely
+ * by a {@link de.uka.ilkd.key.java.reference.TypeReference}.
+ * </DD>
+ * <p>
+ * <DT>References</DT>
+ * <DD>
+ * A {@link de.uka.ilkd.key.java.Reference} is an explicite use of an entity. Most of
+ * these {@link de.uka.ilkd.key.java.Reference}s are
+ * {@link de.uka.ilkd.key.java.reference.NameReference}s
+ * and as such {@link de.uka.ilkd.key.java.NamedProgramElement}s, e.g. the
+ * {@link de.uka.ilkd.key.java.reference.TypeReference}.
+ * Subtypes of {@link de.uka.ilkd.key.java.Reference}s are bundled in the
+ * {@link de.uka.ilkd.key.java.reference} package.
+ * </DD>
+ * <p>
+ * <DT>Modifiers and Declarations</DT>
+ * <DD>
+ * {@link de.uka.ilkd.key.java.declaration.Modifier}s are (exclusively) used in the
+ * context of {@link de.uka.ilkd.key.java.Declaration}s.
+ * {@link de.uka.ilkd.key.java.declaration.Modifier}s occur explicitly, since they occur
+ * as syntactical tokens that might be indented and commented.
+ * {@link de.uka.ilkd.key.java.Declaration}s are either
+ * declarations of types or other entities such as
+ * {@link de.uka.ilkd.key.java.declaration.MemberDeclaration} or
+ * {@link de.uka.ilkd.key.java.declaration.VariableDeclaration}. Concrete
+ * {@link de.uka.ilkd.key.java.declaration.Modifier}s and
+ * {@link de.uka.ilkd.key.java.Declaration}s are
+ * bundled in the {@link de.uka.ilkd.key.java.declaration.modifier} and
+ * {@link de.uka.ilkd.key.java.declaration} packages.
+ * </DD>
+ * </DL>
+ */
+package de.uka.ilkd.key.java;