From 06c37e98d96f8e1b6310f5b177c2909310662b71 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 29 Dec 2023 18:32:58 +0100 Subject: [PATCH 1/2] automatical translate package.html to package-info.java It is recommended since Java 1.5 to use package-info.java. It also allows to set annotation for a whole package (in preparation for nullness checker). --- .../uka/ilkd/key/util/rifl/package-info.java | 8 ++ .../de/uka/ilkd/key/util/rifl/package.html | 17 --- .../key/java/abstraction/package-info.java | 19 +++ .../ilkd/key/java/abstraction/package.html | 27 ---- .../declaration/modifier/package-info.java | 6 + .../java/declaration/modifier/package.html | 14 -- .../key/java/declaration/package-info.java | 11 ++ .../ilkd/key/java/declaration/package.html | 19 --- .../java/expression/literal/package-info.java | 7 + .../key/java/expression/literal/package.html | 15 -- .../expression/operator/package-info.java | 7 + .../key/java/expression/operator/package.html | 15 -- .../key/java/expression/package-info.java | 6 + .../uka/ilkd/key/java/expression/package.html | 14 -- .../de/uka/ilkd/key/java/package-info.java | 103 +++++++++++++ .../java/de/uka/ilkd/key/java/package.html | 110 -------------- .../key/java/recoderext/adt/package-info.java | 5 + .../ilkd/key/java/recoderext/adt/package.html | 14 -- .../ilkd/key/java/reference/package-info.java | 5 + .../uka/ilkd/key/java/reference/package.html | 13 -- .../ilkd/key/java/statement/package-info.java | 6 + .../uka/ilkd/key/java/statement/package.html | 14 -- .../ilkd/key/java/visitor/package-info.java | 5 + .../de/uka/ilkd/key/java/visitor/package.html | 15 -- .../de/uka/ilkd/key/ldt/package-info.java | 7 + .../java/de/uka/ilkd/key/ldt/package.html | 13 -- .../uka/ilkd/key/logic/op/package-info.java | 20 +++ .../de/uka/ilkd/key/logic/op/package.html | 33 ----- .../de/uka/ilkd/key/logic/package-info.java | 34 +++++ .../java/de/uka/ilkd/key/logic/package.html | 40 ------ .../uka/ilkd/key/logic/sort/package-info.java | 10 ++ .../de/uka/ilkd/key/logic/sort/package.html | 20 --- .../java/de/uka/ilkd/key/pp/package-info.java | 5 + .../main/java/de/uka/ilkd/key/pp/package.html | 14 -- .../uka/ilkd/key/proof/init/package-info.java | 7 + .../de/uka/ilkd/key/proof/init/package.html | 16 --- .../uka/ilkd/key/proof/io/package-info.java | 4 + .../de/uka/ilkd/key/proof/io/package.html | 13 -- .../uka/ilkd/key/proof/mgt/package-info.java | 6 + .../de/uka/ilkd/key/proof/mgt/package.html | 15 -- .../de/uka/ilkd/key/proof/package-info.java | 5 + .../java/de/uka/ilkd/key/proof/package.html | 14 -- .../uka/ilkd/key/rule/inst/package-info.java | 5 + .../de/uka/ilkd/key/rule/inst/package.html | 15 -- .../metaconstruct/arith/package-info.java | 5 + .../key/rule/metaconstruct/arith/package.html | 15 -- .../key/rule/metaconstruct/package-info.java | 5 + .../ilkd/key/rule/metaconstruct/package.html | 15 -- .../de/uka/ilkd/key/rule/package-info.java | 10 ++ .../java/de/uka/ilkd/key/rule/package.html | 16 --- .../de/uka/ilkd/key/smt/package-info.java | 6 + .../java/de/uka/ilkd/key/smt/package.html | 12 -- .../uka/ilkd/key/speclang/package-info.java | 8 ++ .../de/uka/ilkd/key/speclang/package.html | 14 -- .../uka/ilkd/key/strategy/package-info.java | 4 + .../de/uka/ilkd/key/strategy/package.html | 10 -- .../de/uka/ilkd/key/util/package-info.java | 6 + .../java/de/uka/ilkd/key/util/package.html | 12 -- .../de/uka/ilkd/key/util/pp/package-info.java | 25 ++++ .../java/de/uka/ilkd/key/util/pp/package.html | 33 ----- .../key/gui/configuration/package-info.java | 4 + .../ilkd/key/gui/configuration/package.html | 13 -- .../de/uka/ilkd/key/gui/package-info.java | 4 + .../java/de/uka/ilkd/key/gui/package.html | 13 -- .../de/uka/ilkd/key/gui/smt/package-info.java | 4 + .../java/de/uka/ilkd/key/gui/smt/package.html | 13 -- .../recoder/abstraction/package-info.java | 18 +++ .../java/recoder/abstraction/package.html | 17 --- .../java/recoder/bytecode/package-info.java | 6 + .../main/java/recoder/bytecode/package.html | 5 - .../recoder/convenience/package-info.java | 12 ++ .../java/recoder/convenience/package.html | 12 -- .../main/java/recoder/io/package-info.java | 6 + recoder/src/main/java/recoder/io/package.html | 5 - .../declaration/modifier/package-info.java | 6 + .../java/declaration/modifier/package.html | 5 - .../java/declaration/package-info.java | 11 ++ .../recoder/java/declaration/package.html | 10 -- .../java/expression/literal/package-info.java | 7 + .../java/expression/literal/package.html | 6 - .../expression/operator/package-info.java | 7 + .../java/expression/operator/package.html | 6 - .../recoder/java/expression/package-info.java | 6 + .../java/recoder/java/expression/package.html | 5 - .../main/java/recoder/java/package-info.java | 135 ++++++++++++++++++ .../src/main/java/recoder/java/package.html | 134 ----------------- .../recoder/java/reference/package-info.java | 5 + .../java/recoder/java/reference/package.html | 4 - .../recoder/java/statement/package-info.java | 6 + .../java/recoder/java/statement/package.html | 5 - .../main/java/recoder/kit/package-info.java | 9 ++ .../src/main/java/recoder/kit/package.html | 8 -- .../recoder/kit/pattern/package-info.java | 10 ++ .../java/recoder/kit/pattern/package.html | 9 -- .../kit/transformation/package-info.java | 5 + .../recoder/kit/transformation/package.html | 4 - .../main/java/recoder/list/package-info.java | 43 ++++++ .../src/main/java/recoder/list/package.html | 43 ------ .../src/main/java/recoder/package-info.java | 17 +++ recoder/src/main/java/recoder/package.html | 16 --- .../java/recoder/parser/package-info.java | 6 + .../src/main/java/recoder/parser/package.html | 5 - .../java/recoder/service/package-info.java | 4 + .../main/java/recoder/service/package.html | 3 - .../main/java/recoder/util/package-info.java | 8 ++ .../src/main/java/recoder/util/package.html | 7 - .../transformations/util/package-info.java | 8 ++ .../src/transformations/util/package.html | 7 - 108 files changed, 707 insertions(+), 962 deletions(-) create mode 100644 key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java delete mode 100644 key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/declaration/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/expression/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/reference/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/statement/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/visitor/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/ldt/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/sort/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/pp/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/init/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/io/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/proof/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/inst/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/smt/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/speclang/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/util/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/util/package.html create mode 100644 key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/util/pp/package.html create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package.html create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/package.html create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java delete mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package.html create mode 100644 recoder/src/main/java/recoder/abstraction/package-info.java delete mode 100644 recoder/src/main/java/recoder/abstraction/package.html create mode 100644 recoder/src/main/java/recoder/bytecode/package-info.java delete mode 100644 recoder/src/main/java/recoder/bytecode/package.html create mode 100644 recoder/src/main/java/recoder/convenience/package-info.java delete mode 100644 recoder/src/main/java/recoder/convenience/package.html create mode 100644 recoder/src/main/java/recoder/io/package-info.java delete mode 100644 recoder/src/main/java/recoder/io/package.html create mode 100644 recoder/src/main/java/recoder/java/declaration/modifier/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/declaration/modifier/package.html create mode 100644 recoder/src/main/java/recoder/java/declaration/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/declaration/package.html create mode 100644 recoder/src/main/java/recoder/java/expression/literal/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/expression/literal/package.html create mode 100644 recoder/src/main/java/recoder/java/expression/operator/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/expression/operator/package.html create mode 100644 recoder/src/main/java/recoder/java/expression/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/expression/package.html create mode 100644 recoder/src/main/java/recoder/java/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/package.html create mode 100644 recoder/src/main/java/recoder/java/reference/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/reference/package.html create mode 100644 recoder/src/main/java/recoder/java/statement/package-info.java delete mode 100644 recoder/src/main/java/recoder/java/statement/package.html create mode 100644 recoder/src/main/java/recoder/kit/package-info.java delete mode 100644 recoder/src/main/java/recoder/kit/package.html create mode 100644 recoder/src/main/java/recoder/kit/pattern/package-info.java delete mode 100644 recoder/src/main/java/recoder/kit/pattern/package.html create mode 100644 recoder/src/main/java/recoder/kit/transformation/package-info.java delete mode 100644 recoder/src/main/java/recoder/kit/transformation/package.html create mode 100644 recoder/src/main/java/recoder/list/package-info.java delete mode 100644 recoder/src/main/java/recoder/list/package.html create mode 100644 recoder/src/main/java/recoder/package-info.java delete mode 100644 recoder/src/main/java/recoder/package.html create mode 100644 recoder/src/main/java/recoder/parser/package-info.java delete mode 100644 recoder/src/main/java/recoder/parser/package.html create mode 100644 recoder/src/main/java/recoder/service/package-info.java delete mode 100644 recoder/src/main/java/recoder/service/package.html create mode 100644 recoder/src/main/java/recoder/util/package-info.java delete mode 100644 recoder/src/main/java/recoder/util/package.html create mode 100644 recoder/src/test/resources/java5/src/transformations/util/package-info.java delete mode 100644 recoder/src/test/resources/java5/src/transformations/util/package.html diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java new file mode 100644 index 00000000000..7420b91e7b5 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package.html b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package.html deleted file mode 100644 index 5e6d67f1474..00000000000 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package.html +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - -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. - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java new file mode 100644 index 00000000000..a6097492143 --- /dev/null +++ b/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. + *

+ * 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. + *

+ * {@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; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package.html deleted file mode 100644 index dbb6f1ed219..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package.html +++ /dev/null @@ -1,27 +0,0 @@ - - - - - - - - - - -This package contains the meta model 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. -

-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. -

-{@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. - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java new file mode 100644 index 00000000000..0d1cddbc5cd --- /dev/null +++ b/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; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package.html deleted file mode 100644 index 2b53bd6c867..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -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}. - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java new file mode 100644 index 00000000000..d7764b669e9 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package.html deleted file mode 100644 index ce67e7abf02..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package.html +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - - -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}. - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java new file mode 100644 index 00000000000..1a2c375c966 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package.html deleted file mode 100644 index fcba032dbd0..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - - - -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}. - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java new file mode 100644 index 00000000000..583fd4cbc12 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package.html deleted file mode 100644 index bd58f308a00..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - - - -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}). - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java new file mode 100644 index 00000000000..ee80e567e01 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/expression/package.html deleted file mode 100644 index 0b1754d1697..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -Elements of the Java syntax tree representing expressions. -The various operators and literals are bundled in the corresponding -subpackages. - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java new file mode 100644 index 00000000000..5ae7d044d74 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java @@ -0,0 +1,103 @@ +/** + * 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. + *

+ *
Source and Program Elements
+ *
+ * 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}. + *

+ * 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. + *

+ * {@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}. + *

+ * {@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}. + *

+ *

+ *

Expressions and Statements
+ *
+ * {@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}). + *

+ * 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. + *

+ *

+ *

Syntax Tree Parents
+ *
+ * There are a couple of abstractions dealing with properties of being a + * parent node. + *

+ * 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}. + *

+ *

+ *

References
+ *
+ * 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. + *
+ *

+ *

Modifiers and Declarations
+ *
+ * {@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. + *
+ *
+ */ +package de.uka.ilkd.key.java; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/package.html deleted file mode 100644 index 521efb59acf..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/package.html +++ /dev/null @@ -1,110 +0,0 @@ - - - - - - - -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. -
-
Source and Program Elements
-
-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}. -

-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. -

-{@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}. -

-{@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}. -

-

-

Expressions and Statements
-
-{@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}). -

-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. -

-

-

Syntax Tree Parents
-
-There are a couple of abstractions dealing with properties of being a -parent node. -

-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}. -

-

-

References
-
-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. -
-

-

Modifiers and Declarations
-
-{@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. -
-
- diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java new file mode 100644 index 00000000000..2a28f741f15 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java @@ -0,0 +1,5 @@ +/** + * This package contains RecodeR Operators + * which represent algebraic data type functions. (See also the ldt package description.) + */ +package de.uka.ilkd.key.java.recoderext.adt; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package.html deleted file mode 100644 index e969bb108bb..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -This package contains RecodeR Operators -which represent algebraic data type functions. (See also the ldt package description.) - - \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java new file mode 100644 index 00000000000..3d8cb9af65c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java @@ -0,0 +1,5 @@ +/** + * Elements of the Java syntax tree representing implicit or explicit (named) + * references to other program elements. + */ +package de.uka.ilkd.key.java.reference; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/reference/package.html deleted file mode 100644 index 5af2300c18d..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/package.html +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - -Elements of the Java syntax tree representing implicit or explicit (named) -references to other program elements. - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java new file mode 100644 index 00000000000..673dd6ba5e9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java @@ -0,0 +1,6 @@ +/** + * Elements of the Java syntax tree representing pure statements. + * Besides these other valid statements are the various expressions with + * side effects ({@link recoder.java.expression.ExpressionStatement}s). + */ +package de.uka.ilkd.key.java.statement; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/statement/package.html deleted file mode 100644 index 86b77166ec3..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -Elements of the Java syntax tree representing pure statements. -Besides these other valid statements are the various expressions with -side effects ({@link recoder.java.expression.ExpressionStatement}s). - diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java new file mode 100644 index 00000000000..40c024d906f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java @@ -0,0 +1,5 @@ +/** + * contains classes representing visitors traversing the tree + * structure of Java programs. + */ +package de.uka.ilkd.key.java.visitor; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package.html b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package.html deleted file mode 100644 index c5ff243d38b..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - contains classes representing visitors traversing the tree - structure of Java programs. - - -Last modified: Tue Nov 26 08:54:55 MET 2002 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java new file mode 100644 index 00000000000..c009262e6c5 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java @@ -0,0 +1,7 @@ +/** + * This package contains the "language data types" (LDTs) of KeY. LDTs + * correspond to standard rule files shipped with KeY, and provide a + * programming interface to access the entities declared in these + * rule files. + */ +package de.uka.ilkd.key.ldt; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/package.html b/key.core/src/main/java/de/uka/ilkd/key/ldt/package.html deleted file mode 100644 index fd05c2ef99a..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/package.html +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - This package contains the "language data types" (LDTs) of KeY. LDTs - correspond to standard rule files shipped with KeY, and provide a - programming interface to access the entities declared in these - rule files. - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java new file mode 100644 index 00000000000..2d10005e5e6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java @@ -0,0 +1,20 @@ +/** + * contains the operators of {@link + * de.uka.ilkd.key.logic.Term}s. Operators may be {@link + * de.uka.ilkd.key.logic.op.Quantifier}s or {@link + * de.uka.ilkd.key.logic.op.SubstOp}s that bind variables for + * subterms, but also {@link de.uka.ilkd.key.logic.op.Modality}s, or + * {@link de.uka.ilkd.key.logic.op.QuanUpdateOperator}s. Many of the operators + * are constantly defined in {@link de.uka.ilkd.key.logic.op.Op}s. + * An operator can be a {@link de.uka.ilkd.key.logic.op.TermSymbol}s, + * such as a {@link de.uka.ilkd.key.logic.op.Function} or a + * variable. There are several kind of variables: {@link + * de.uka.ilkd.key.logic.op.LogicVariable}s (variables that must be + * bound but do not occur in programs), {@link + * de.uka.ilkd.key.logic.op.ProgramVariable}s (allowed both in + * programs and in logic, but not boundable), {@link + * de.uka.ilkd.key.logic.op.Metavariable}s, and {@link + * de.uka.ilkd.key.logic.op.SchemaVariable}s for {@link + * de.uka.ilkd.key.rule.Taclet}s. + */ +package de.uka.ilkd.key.logic.op; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/package.html b/key.core/src/main/java/de/uka/ilkd/key/logic/op/package.html deleted file mode 100644 index a20b86843e9..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/package.html +++ /dev/null @@ -1,33 +0,0 @@ - - - - - - - - contains the operators of {@link - de.uka.ilkd.key.logic.Term}s. Operators may be {@link - de.uka.ilkd.key.logic.op.Quantifier}s or {@link - de.uka.ilkd.key.logic.op.SubstOp}s that bind variables for - subterms, but also {@link de.uka.ilkd.key.logic.op.Modality}s, or - {@link de.uka.ilkd.key.logic.op.QuanUpdateOperator}s. Many of the operators - are constantly defined in {@link de.uka.ilkd.key.logic.op.Op}s. - - An operator can be a {@link de.uka.ilkd.key.logic.op.TermSymbol}s, - such as a {@link de.uka.ilkd.key.logic.op.Function} or a - variable. There are several kind of variables: {@link - de.uka.ilkd.key.logic.op.LogicVariable}s (variables that must be - bound but do not occur in programs), {@link - de.uka.ilkd.key.logic.op.ProgramVariable}s (allowed both in - programs and in logic, but not boundable), {@link - de.uka.ilkd.key.logic.op.Metavariable}s, and {@link - de.uka.ilkd.key.logic.op.SchemaVariable}s for {@link - de.uka.ilkd.key.rule.Taclet}s. - - - - -Last modified: Mon Apr 18 09:42:36 MEST 2005 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java new file mode 100644 index 00000000000..b0ab26c0d33 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java @@ -0,0 +1,34 @@ +/** + *

provides a representation for the term and sequent + * structure. The structure of a term is defined in {@link + * de.uka.ilkd.key.logic.Term}. Subclasses of {@link + * de.uka.ilkd.key.logic.Term} provide representations for special + * kinds of terms. However, these subclasses are supposed to be not + * directly accessed. Instead, {@link de.uka.ilkd.key.logic.Term} + * provides methods for all the methods of the + * subclasses. Moreover, {@link de.uka.ilkd.key.logic.Term}s (or + * their subclasses) are supposed to be never constructed by + * constructors of their own, but by instances of {@link + * de.uka.ilkd.key.logic.TermFactory}.

+ *

The function of {@link de.uka.ilkd.key.logic.Term}s (e.g., if + * they represent a conjunction of subterms, a quantified + * formula,...) is only determined by an {@link + * de.uka.ilkd.key.logic.op.Operator} that is assigned to a {@link + * de.uka.ilkd.key.logic.Term} when the {@link + * de.uka.ilkd.key.logic.Term} is constructed.

+ *

{@link de.uka.ilkd.key.logic.Sequent}s consist of two {@link + * de.uka.ilkd.key.logic.Semisequent}s which represent a + * duplicate-free list of a {@link + * de.uka.ilkd.key.logic.SequentFormula}s. The latter consist of + * a {@link de.uka.ilkd.key.logic.Constraint} and a {@link + * de.uka.ilkd.key.logic.Term} of a special sort {@link + * de.uka.ilkd.key.logic.sort.Sort#FORMULA}.

+ *

{@link de.uka.ilkd.key.logic.Sequent}s and {@link + * de.uka.ilkd.key.logic.Term}s are immutable. + *

+ * + * + * Last modified: Wed Dec 4 15:11:14 MET 2002 + * + */ +package de.uka.ilkd.key.logic; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/package.html b/key.core/src/main/java/de/uka/ilkd/key/logic/package.html deleted file mode 100644 index 9e3c6a8d23f..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/package.html +++ /dev/null @@ -1,40 +0,0 @@ - - - - - - - -

provides a representation for the term and sequent - structure. The structure of a term is defined in {@link - de.uka.ilkd.key.logic.Term}. Subclasses of {@link - de.uka.ilkd.key.logic.Term} provide representations for special - kinds of terms. However, these subclasses are supposed to be not - directly accessed. Instead, {@link de.uka.ilkd.key.logic.Term} - provides methods for all the methods of the - subclasses. Moreover, {@link de.uka.ilkd.key.logic.Term}s (or - their subclasses) are supposed to be never constructed by - constructors of their own, but by instances of {@link - de.uka.ilkd.key.logic.TermFactory}.

-

The function of {@link de.uka.ilkd.key.logic.Term}s (e.g., if - they represent a conjunction of subterms, a quantified - formula,...) is only determined by an {@link - de.uka.ilkd.key.logic.op.Operator} that is assigned to a {@link - de.uka.ilkd.key.logic.Term} when the {@link - de.uka.ilkd.key.logic.Term} is constructed.

-

{@link de.uka.ilkd.key.logic.Sequent}s consist of two {@link - de.uka.ilkd.key.logic.Semisequent}s which represent a - duplicate-free list of a {@link - de.uka.ilkd.key.logic.SequentFormula}s. The latter consist of - a {@link de.uka.ilkd.key.logic.Constraint} and a {@link - de.uka.ilkd.key.logic.Term} of a special sort {@link - de.uka.ilkd.key.logic.sort.Sort#FORMULA}.

-

{@link de.uka.ilkd.key.logic.Sequent}s and {@link - de.uka.ilkd.key.logic.Term}s are immutable. - - - -Last modified: Wed Dec 4 15:11:14 MET 2002 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java new file mode 100644 index 00000000000..5511d09c41d --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java @@ -0,0 +1,10 @@ +/** + * This package contains different kinds and implementations subtyping interface Sort. + * Each logic term has an assigned a sort. In order to support special concepts like + * arrays, objects, primitive types, it is useful to support different kinds of sorts. + * This allows to distinguish diffent categories of terms by looking on the sort type + * rather than on the name. + * In KeY we distinguish formulas from terms by the special sort instance + * Sort.Formula. + */ +package de.uka.ilkd.key.logic.sort; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package.html b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package.html deleted file mode 100644 index ed74b17e3c5..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package.html +++ /dev/null @@ -1,20 +0,0 @@ - - - - - - - - This package contains different kinds and implementations subtyping interface Sort. - Each logic term has an assigned a sort. In order to support special concepts like - arrays, objects, primitive types, it is useful to support different kinds of sorts. - This allows to distinguish diffent categories of terms by looking on the sort type - rather than on the name. - In KeY we distinguish formulas from terms by the special sort instance - Sort.Formula. - - -Last modified: Tue Nov 26 08:54:55 MET 2002 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java new file mode 100644 index 00000000000..8cd2b762bbd --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java @@ -0,0 +1,5 @@ +/** + * This package contains pretty-printing functionality used by the GUI and for + * saving proofs. + */ +package de.uka.ilkd.key.pp; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/package.html b/key.core/src/main/java/de/uka/ilkd/key/pp/package.html deleted file mode 100644 index 6d5ceeabe86..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -This package contains pretty-printing functionality used by the GUI and for -saving proofs. - - \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java new file mode 100644 index 00000000000..414abffbb7a --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java @@ -0,0 +1,7 @@ +/** + * This package contains classes handling prover initialisation. ProblemInitializer + * is the main class that drives the initialisation process. Core interfaces are + * EnvInput (provides a proof environment) and ProofOblInput (provides one or many + * sequents whose validity is to be proven). + */ +package de.uka.ilkd.key.proof.init; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/package.html b/key.core/src/main/java/de/uka/ilkd/key/proof/init/package.html deleted file mode 100644 index 181598226dd..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/package.html +++ /dev/null @@ -1,16 +0,0 @@ - - - - - - - - - - -This package contains classes handling prover initialisation. ProblemInitializer -is the main class that drives the initialisation process. Core interfaces are -EnvInput (provides a proof environment) and ProofOblInput (provides one or many -sequents whose validity is to be proven). - - \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java new file mode 100644 index 00000000000..1276060d13b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java @@ -0,0 +1,4 @@ +/** + * Classes related to loading and saving proof files. + */ +package de.uka.ilkd.key.proof.io; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/package.html b/key.core/src/main/java/de/uka/ilkd/key/proof/io/package.html deleted file mode 100644 index 4e2e773ca2c..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/package.html +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - -Classes related to loading and saving proof files. - - \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java new file mode 100644 index 00000000000..94a92e3a217 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java @@ -0,0 +1,6 @@ +/** + * This package contains classes for proof environments and proof management. For + * example, proof management ensures that contract applications cannot lead to + * unsound cyclic dependencies between proofs. + */ +package de.uka.ilkd.key.proof.mgt; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package.html b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package.html deleted file mode 100644 index 34cebdc1c0b..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - - - -This package contains classes for proof environments and proof management. For -example, proof management ensures that contract applications cannot lead to -unsound cyclic dependencies between proofs. - - \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java new file mode 100644 index 00000000000..bbcf3c62f5a --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java @@ -0,0 +1,5 @@ +/** + * This package contains the core data structures of proofs, nodes, goals, as well + * as machinery to deal with these data structures. + */ +package de.uka.ilkd.key.proof; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/package.html b/key.core/src/main/java/de/uka/ilkd/key/proof/package.html deleted file mode 100644 index 47d0dc81366..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -This package contains the core data structures of proofs, nodes, goals, as well -as machinery to deal with these data structures. - - \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java new file mode 100644 index 00000000000..1a0ec2117a2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java @@ -0,0 +1,5 @@ +/** + * contains classes for the instantiation of schema variables of {@link + * de.uka.ilkd.key.rule.Taclet}s. + */ +package de.uka.ilkd.key.rule.inst; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package.html b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package.html deleted file mode 100644 index ef0bb0021dd..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - contains classes for the instantiation of schema variables of {@link - de.uka.ilkd.key.rule.Taclet}s. - - -Last modified: Tue Nov 26 08:54:55 MET 2002 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java new file mode 100644 index 00000000000..a13bae15f8f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java @@ -0,0 +1,5 @@ +/** + * contains classes representing the special meta constructs of {@link + * de.uka.ilkd.key.rule.Taclet}s performing arithmetic operations. + */ +package de.uka.ilkd.key.rule.metaconstruct.arith; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package.html b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package.html deleted file mode 100644 index fb3af1a963f..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - contains classes representing the special meta constructs of {@link - de.uka.ilkd.key.rule.Taclet}s performing arithmetic operations. - - -Last modified: Tue Nov 26 08:54:55 MET 2002 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java new file mode 100644 index 00000000000..753f96f9e56 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java @@ -0,0 +1,5 @@ +/** + * contains classes representing the meta constructs of {@link + * de.uka.ilkd.key.rule.Taclet}s. + */ +package de.uka.ilkd.key.rule.metaconstruct; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package.html b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package.html deleted file mode 100644 index e78443a483a..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package.html +++ /dev/null @@ -1,15 +0,0 @@ - - - - - - - - contains classes representing the meta constructs of {@link - de.uka.ilkd.key.rule.Taclet}s. - - -Last modified: Tue Nov 26 08:54:55 MET 2002 - - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java new file mode 100644 index 00000000000..6e7df2eb20e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java @@ -0,0 +1,10 @@ +/** + * This package contains classes for implementing rules. Most rules are + * taclet rules, represented by {@link + * de.uka.ilkd.key.rule.Taclet}. The package includes the + * representation of applications of taclets ({@link + * de.uka.ilkd.key.rule.TacletApp}) and the builders of taclets ({@link + * de.uka.ilkd.key.rule.TacletBuilder}). Besides taclets, there are + * built-in rules implemented directly in Java. + */ +package de.uka.ilkd.key.rule; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/package.html b/key.core/src/main/java/de/uka/ilkd/key/rule/package.html deleted file mode 100644 index c5626c58d39..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/package.html +++ /dev/null @@ -1,16 +0,0 @@ - - - - - - - - This package contains classes for implementing rules. Most rules are - taclet rules, represented by {@link - de.uka.ilkd.key.rule.Taclet}. The package includes the - representation of applications of taclets ({@link - de.uka.ilkd.key.rule.TacletApp}) and the builders of taclets ({@link - de.uka.ilkd.key.rule.TacletBuilder}). Besides taclets, there are - built-in rules implemented directly in Java. - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java new file mode 100644 index 00000000000..5d7738b7b01 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java @@ -0,0 +1,6 @@ +/** + * This package contains the SMT backend of KeY, allowing to translate KeY formulas + * to formulas in formats such as SMT-LIB, and allowing to send such formulas to + * SMT solvers such as Simplify or Z3. + */ +package de.uka.ilkd.key.smt; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/package.html b/key.core/src/main/java/de/uka/ilkd/key/smt/package.html deleted file mode 100644 index c6bf0fce73f..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/package.html +++ /dev/null @@ -1,12 +0,0 @@ - - - - - - - - This package contains the SMT backend of KeY, allowing to translate KeY formulas - to formulas in formats such as SMT-LIB, and allowing to send such formulas to - SMT solvers such as Simplify or Z3. - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java new file mode 100644 index 00000000000..86674f87011 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java @@ -0,0 +1,8 @@ +/** + * This package contains the specification language frontends of KeY. The task + * of the individual frontends (locates in subpackages such as "jml"), is to + * create objects of the types declared in this package. Core types are Contract, + * OperationContract, and DependencyContract. These are used as input by the + * proof obligations declared in package proof.init. + */ +package de.uka.ilkd.key.speclang; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/package.html b/key.core/src/main/java/de/uka/ilkd/key/speclang/package.html deleted file mode 100644 index 2e215ba8f38..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/package.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - This package contains the specification language frontends of KeY. The task - of the individual frontends (locates in subpackages such as "jml"), is to - create objects of the types declared in this package. Core types are Contract, - OperationContract, and DependencyContract. These are used as input by the - proof obligations declared in package proof.init. - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java new file mode 100644 index 00000000000..93c5d20544c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java @@ -0,0 +1,4 @@ +/** + * This package contains classes implementing the proof search strategies of KeY. + */ +package de.uka.ilkd.key.strategy; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/package.html b/key.core/src/main/java/de/uka/ilkd/key/strategy/package.html deleted file mode 100644 index 3c3bf47bfff..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/package.html +++ /dev/null @@ -1,10 +0,0 @@ - - - - - - - - This package contains classes implementing the proof search strategies of KeY. - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java new file mode 100644 index 00000000000..6ca9c1ca0ac --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java @@ -0,0 +1,6 @@ +/** + * This package is a grab bag of miscellaneous useful code fragments. It also contains + * side functionalities like the installer (subpackage install), and the tool for + * removing generics from a Java program (subpackage removegenerics). + */ +package de.uka.ilkd.key.util; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/package.html b/key.core/src/main/java/de/uka/ilkd/key/util/package.html deleted file mode 100644 index 910f9a59c9b..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/util/package.html +++ /dev/null @@ -1,12 +0,0 @@ - - - - - - - - This package is a grab bag of miscellaneous useful code fragments. It also contains - side functionalities like the installer (subpackage install), and the tool for - removing generics from a Java program (subpackage removegenerics). - - diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java new file mode 100644 index 00000000000..ac450158480 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java @@ -0,0 +1,25 @@ +/** + * A package to pretty-print information using line breaks and + * indentation. For instance, it can be used to print + * 

+ * while (i>0) {
+ * i--;
+ * j++;
+ * }
+ *
+ * instead of + * 
+ * while (i>0) { i
+ * --; j++;}
+ *
+ * if a maximum line width of 15 characters is chosen. The frontend + * to the Pretty-Printer is the {@link + * de.uka.ilkd.key.util.pp.Layouter} class. You may configure what + * happens with the output by implemenenting the {@link + * de.uka.ilkd.key.util.pp.Backend} interface, or by using the + * standard implementation {@link + * de.uka.ilkd.key.util.pp.StringBackend}. + * + * @author Martin Giese + */ +package de.uka.ilkd.key.util.pp; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/pp/package.html b/key.core/src/main/java/de/uka/ilkd/key/util/pp/package.html deleted file mode 100644 index 50cd4017f91..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/util/pp/package.html +++ /dev/null @@ -1,33 +0,0 @@ - - - - - - - - - - A package to pretty-print information using line breaks and - indentation. For instance, it can be used to print - 
-    while (i>0) {
-      i--;
-      j++;
-    }
-
- instead of - 
-    while (i>0) { i
-    --; j++;}
-
- if a maximum line width of 15 characters is chosen. The frontend - to the Pretty-Printer is the {@link - de.uka.ilkd.key.util.pp.Layouter} class. You may configure what - happens with the output by implemenenting the {@link - de.uka.ilkd.key.util.pp.Backend} interface, or by using the - standard implementation {@link - de.uka.ilkd.key.util.pp.StringBackend}. - - @author Martin Giese - - diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java new file mode 100644 index 00000000000..3e6b71238db --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java @@ -0,0 +1,4 @@ +/** + * This package contains classes to do with the configuration / settings of KeY. + */ +package de.uka.ilkd.key.gui.configuration; \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package.html b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package.html deleted file mode 100644 index 76bd7c6dec5..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package.html +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - -This package contains classes to do with the configuration / settings of KeY. - - \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java new file mode 100644 index 00000000000..9a0f762150f --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java @@ -0,0 +1,4 @@ +/** + * This package contains classes forming the graphical user interface of KeY. + */ +package de.uka.ilkd.key.gui; \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/package.html b/key.ui/src/main/java/de/uka/ilkd/key/gui/package.html deleted file mode 100644 index 64175fb5d29..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/package.html +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - -This package contains classes forming the graphical user interface of KeY. - - \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java new file mode 100644 index 00000000000..e9af4b204b1 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java @@ -0,0 +1,4 @@ +/** + * This package contains the graphical user interface of the SMT backend. + */ +package de.uka.ilkd.key.gui.smt; \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package.html b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package.html deleted file mode 100644 index 17096586f5c..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package.html +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - -This package contains the graphical user interface of the SMT backend. - - \ No newline at end of file diff --git a/recoder/src/main/java/recoder/abstraction/package-info.java b/recoder/src/main/java/recoder/abstraction/package-info.java new file mode 100644 index 00000000000..e6735125ac2 --- /dev/null +++ b/recoder/src/main/java/recoder/abstraction/package-info.java @@ -0,0 +1,18 @@ +/** + * This package contains the meta model 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. + *

+ * 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. + *

+ * {@link recoder.java.ScopeDefiningElement}s are initialized by + * {@link recoder.service.SourceInfo} implementations; the corresponding + * methods should not be uses by others. + */ +package recoder.abstraction; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/abstraction/package.html b/recoder/src/main/java/recoder/abstraction/package.html deleted file mode 100644 index 75cad5cd27c..00000000000 --- a/recoder/src/main/java/recoder/abstraction/package.html +++ /dev/null @@ -1,17 +0,0 @@ - -This package contains the meta model 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. -

- 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. -

- {@link recoder.java.ScopeDefiningElement}s are initialized by - {@link recoder.service.SourceInfo} implementations; the corresponding - methods should not be uses by others. - diff --git a/recoder/src/main/java/recoder/bytecode/package-info.java b/recoder/src/main/java/recoder/bytecode/package-info.java new file mode 100644 index 00000000000..b1c78d78859 --- /dev/null +++ b/recoder/src/main/java/recoder/bytecode/package-info.java @@ -0,0 +1,6 @@ +/** + * This package contains classes that cover information derived from Java byte + * code. As RECODER does not rewrite Bytecode, the information remains on + * interface level - no statements are analyzed. + */ +package recoder.bytecode; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/bytecode/package.html b/recoder/src/main/java/recoder/bytecode/package.html deleted file mode 100644 index a9e07816b86..00000000000 --- a/recoder/src/main/java/recoder/bytecode/package.html +++ /dev/null @@ -1,5 +0,0 @@ - -This package contains classes that cover information derived from Java byte -code. As RECODER does not rewrite Bytecode, the information remains on -interface level - no statements are analyzed. - diff --git a/recoder/src/main/java/recoder/convenience/package-info.java b/recoder/src/main/java/recoder/convenience/package-info.java new file mode 100644 index 00000000000..af9b49f1123 --- /dev/null +++ b/recoder/src/main/java/recoder/convenience/package-info.java @@ -0,0 +1,12 @@ +/** + * The convenience layer contains auxiliary functions that are useful in + * the context of RECODER. + *

+ */ +package recoder.convenience; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/convenience/package.html b/recoder/src/main/java/recoder/convenience/package.html deleted file mode 100644 index 5400b846220..00000000000 --- a/recoder/src/main/java/recoder/convenience/package.html +++ /dev/null @@ -1,12 +0,0 @@ - -The convenience layer contains auxiliary functions that are useful in -the context of RECODER. - - - diff --git a/recoder/src/main/java/recoder/io/package-info.java b/recoder/src/main/java/recoder/io/package-info.java new file mode 100644 index 00000000000..98e7604ae82 --- /dev/null +++ b/recoder/src/main/java/recoder/io/package-info.java @@ -0,0 +1,6 @@ +/** + * The io package provides classes to import and export source and class files. + * The abstractions hide where the information stems from or should go to, + * e.g. files with various file formats, databases or graphical interfaces. + */ +package recoder.io; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/io/package.html b/recoder/src/main/java/recoder/io/package.html deleted file mode 100644 index 9f79e194c40..00000000000 --- a/recoder/src/main/java/recoder/io/package.html +++ /dev/null @@ -1,5 +0,0 @@ - -The io package provides classes to import and export source and class files. -The abstractions hide where the information stems from or should go to, -e.g. files with various file formats, databases or graphical interfaces. - diff --git a/recoder/src/main/java/recoder/java/declaration/modifier/package-info.java b/recoder/src/main/java/recoder/java/declaration/modifier/package-info.java new file mode 100644 index 00000000000..ce1ef2e01d7 --- /dev/null +++ b/recoder/src/main/java/recoder/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 recoder.java.declaration.modifier; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/declaration/modifier/package.html b/recoder/src/main/java/recoder/java/declaration/modifier/package.html deleted file mode 100644 index 8e49748a0d7..00000000000 --- a/recoder/src/main/java/recoder/java/declaration/modifier/package.html +++ /dev/null @@ -1,5 +0,0 @@ - -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}. - diff --git a/recoder/src/main/java/recoder/java/declaration/package-info.java b/recoder/src/main/java/recoder/java/declaration/package-info.java new file mode 100644 index 00000000000..d64a7973b16 --- /dev/null +++ b/recoder/src/main/java/recoder/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 recoder.java.declaration; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/declaration/package.html b/recoder/src/main/java/recoder/java/declaration/package.html deleted file mode 100644 index 96b95d839ae..00000000000 --- a/recoder/src/main/java/recoder/java/declaration/package.html +++ /dev/null @@ -1,10 +0,0 @@ - -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}. - diff --git a/recoder/src/main/java/recoder/java/expression/literal/package-info.java b/recoder/src/main/java/recoder/java/expression/literal/package-info.java new file mode 100644 index 00000000000..c87f527e517 --- /dev/null +++ b/recoder/src/main/java/recoder/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 recoder.java.expression.literal; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/expression/literal/package.html b/recoder/src/main/java/recoder/java/expression/literal/package.html deleted file mode 100644 index 8ec441a6bcd..00000000000 --- a/recoder/src/main/java/recoder/java/expression/literal/package.html +++ /dev/null @@ -1,6 +0,0 @@ - -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}. - diff --git a/recoder/src/main/java/recoder/java/expression/operator/package-info.java b/recoder/src/main/java/recoder/java/expression/operator/package-info.java new file mode 100644 index 00000000000..13d009834f9 --- /dev/null +++ b/recoder/src/main/java/recoder/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 recoder.java.expression.operator; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/expression/operator/package.html b/recoder/src/main/java/recoder/java/expression/operator/package.html deleted file mode 100644 index 00f1d5cb75c..00000000000 --- a/recoder/src/main/java/recoder/java/expression/operator/package.html +++ /dev/null @@ -1,6 +0,0 @@ - -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}). - diff --git a/recoder/src/main/java/recoder/java/expression/package-info.java b/recoder/src/main/java/recoder/java/expression/package-info.java new file mode 100644 index 00000000000..6e426b0b81c --- /dev/null +++ b/recoder/src/main/java/recoder/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 recoder.java.expression; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/expression/package.html b/recoder/src/main/java/recoder/java/expression/package.html deleted file mode 100644 index 1d82f6c92f0..00000000000 --- a/recoder/src/main/java/recoder/java/expression/package.html +++ /dev/null @@ -1,5 +0,0 @@ - -Elements of the Java syntax tree representing expressions. -The various operators and literals are bundled in the corresponding -subpackages. - diff --git a/recoder/src/main/java/recoder/java/package-info.java b/recoder/src/main/java/recoder/java/package-info.java new file mode 100644 index 00000000000..3dfa4049eab --- /dev/null +++ b/recoder/src/main/java/recoder/java/package-info.java @@ -0,0 +1,135 @@ +/** + * This package contains classes that cover the Java programming language. + * These classes are fundamental for syntactical transformations and deserve + * a detailed overview. + *
+ *
Source and Program Elements
+ *
+ * A {@link recoder.java.SourceElement} is a syntactical entity and not + * necessary a {@link recoder.ModelElement}, such as a {@link recoder.java.Comment}. + * Each {@link recoder.java.SourceElement} knows its + * {@link recoder.ProgramFactory}, its indentation and how to + * {@link recoder.java.SourceElement#deepClone} itself. + *

+ * A {@link recoder.java.ProgramElement} is a {@link recoder.java.SourceElement} + * and a {@link recoder.ModelElement}. It is aware of its parent in the syntax + * tree, while a pure {@link recoder.java.SourceElement} is not considered as a + * member of the AST even though it is represented in the sources. + *

+ * {@link recoder.java.ProgramElement}s are further + * classified into {@link recoder.java.TerminalProgramElement}s and + * {@link recoder.java.NonTerminalProgramElement}s (this is another + * Composite pattern). While {@link recoder.java.TerminalProgramElement} + * is just a tag class, {@link recoder.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 recoder.java.CompilationUnit}. + *

+ * {@link recoder.java.JavaSourceElement} and + * {@link recoder.java.JavaProgramElement} are abstract classes defining + * standard implementations that already know their + * {@link recoder.java.JavaProgramFactory}. + *

+ *

+ *

Validation
+ *
+ * Calling the {@link recoder.ModelElement#validate()} method of a + * {@link recoder.ModelElement} will check its consistency similar to the + * analysis a compiler does. In case of an inconsistency, a + * {@link recoder.ModelException} is thrown. The + * {@link recoder.ModelElement#validate()} method of a + * {@link recoder.java.ProgramElement} will check its children if + * necessary. Calling {@link recoder.ModelElement#validate()} for a + * {@link recoder.java.CompilationUnit} will check the consistency of the + * whole module. + *

+ * A {@link recoder.java.NonTerminalProgramElement} defines a + * {@link recoder.java.NonTerminalProgramElement#makeParentRoleValid()} method + * that sets all parent links of the current children. Not that a + * {@link recoder.java.SourceElement} automatically keeps track of any attached + * {@link recoder.java.Comment}. + * The method is automatically invoked by each constructor that creates a + * concrete and valid program element. Since some constructors create + * partially initialized nodes only, there is no need to make them valid at + * that time. + *

+ *

+ *

Expressions and Statements
+ *
+ * {@link recoder.java.Expression} and {@link recoder.java.Statement} are + * self-explanatory. A {@link recoder.java.LoopInitializer} is a special + * {@link recoder.java.Statement} valid as initializer of + * {@link recoder.java.statement.For} loops. + * {@link recoder.java.LoopInitializer} is subtyped by + * {@link recoder.java.expression.ExpressionStatement} and + * {@link recoder.java.declaration.LocalVariableDeclaration}). + *

+ * Concrete classes and further abstractions are bundled in the + * {@link recoder.java.expression} and {@link recoder.java.statement} packages. + *

+ *

+ *

Syntax Tree Parents
+ *
+ * There are a couple of abstractions dealing with properties of being a + * parent node, which is used for upwards traversals in the syntax tree. + *

+ * These are {@link recoder.java.declaration.TypeDeclarationContainer}, + * {@link recoder.java.ExpressionContainer}, + * {@link recoder.java.StatementContainer}, + * {@link recoder.java.ParameterContainer}, + * {@link recoder.java.NamedProgramElement} and + * {@link recoder.java.reference.TypeReferenceContainer}. A + * An {@link recoder.java.ExpressionContainer} contains + * {@link recoder.java.Expression}s, a + * {@link recoder.java.StatementContainer} contains + * {@link recoder.java.Statement}s, a + * {@link recoder.java.ParameterContainer} + * (either a {@link recoder.java.declaration.MethodDeclaration} or a + * {@link recoder.java.statement.Catch} statement) contains + * {@link recoder.java.declaration.ParameterDeclaration}s. + * A {@link recoder.java.NamedProgramElement} is a subtype of + * {@link recoder.NamedModelElement}. + * A {@link recoder.java.reference.TypeReferenceContainer} contains one or + * several names, but these are names of types that are referred to explicitely + * by a {@link recoder.java.reference.TypeReference}. + *

+ *

+ *

References
+ *
+ * A {@link recoder.java.Reference} is an explicite use of an entity. Most of + * these {@link recoder.java.Reference}s are + * {@link recoder.java.reference.NameReference}s + * and as such {@link recoder.java.NamedProgramElement}s, e.g. the + * {@link recoder.java.reference.TypeReference}. + * Subtypes of {@link recoder.java.Reference}s are bundled in the + * {@link recoder.java.reference} package. + *
+ *

+ *

Modifiers and Declarations
+ *
+ * {@link recoder.java.declaration.Modifier}s are (exclusively) used in the + * context of {@link recoder.java.Declaration}s. + * {@link recoder.java.declaration.Modifier}s occur explictely, since they occur + * as syntactical tokens that might be indented and commented. + * {@link recoder.java.Declaration}s are either + * declarations of types or other entities such as + * {@link recoder.java.declaration.MemberDeclaration} or + * {@link recoder.java.declaration.VariableDeclaration}. Concrete + * {@link recoder.java.declaration.Modifier}s and + * {@link recoder.java.Declaration}s are + * bundled in the {@link recoder.java.declaration.modifier} and + * {@link recoder.java.declaration} packages. + *
+ *

+ *

Comments
+ *
+ * A {@link recoder.java.ProgramElement} can have a list of + * {@link recoder.java.Comment}s attached. + *

+ * While a pure {@link recoder.java.Comment} can extend to several lines, a + * {@link recoder.java.SingleLineComment} may not contain linefeeds. + * A {@link recoder.java.DocComment} is a special comment used for + * documentation systems such as JavaDoc or DOC++. + *

+ *
+ */ +package recoder.java; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/package.html b/recoder/src/main/java/recoder/java/package.html deleted file mode 100644 index 4ad739db144..00000000000 --- a/recoder/src/main/java/recoder/java/package.html +++ /dev/null @@ -1,134 +0,0 @@ - -This package contains classes that cover the Java programming language. -These classes are fundamental for syntactical transformations and deserve -a detailed overview. -
-
Source and Program Elements
-
- A {@link recoder.java.SourceElement} is a syntactical entity and not - necessary a {@link recoder.ModelElement}, such as a {@link recoder.java.Comment}. - Each {@link recoder.java.SourceElement} knows its - {@link recoder.ProgramFactory}, its indentation and how to - {@link recoder.java.SourceElement#deepClone} itself. -

- A {@link recoder.java.ProgramElement} is a {@link recoder.java.SourceElement} - and a {@link recoder.ModelElement}. It is aware of its parent in the syntax - tree, while a pure {@link recoder.java.SourceElement} is not considered as a - member of the AST even though it is represented in the sources. -

- {@link recoder.java.ProgramElement}s are further - classified into {@link recoder.java.TerminalProgramElement}s and - {@link recoder.java.NonTerminalProgramElement}s (this is another - Composite pattern). While {@link recoder.java.TerminalProgramElement} - is just a tag class, {@link recoder.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 recoder.java.CompilationUnit}. -

- {@link recoder.java.JavaSourceElement} and - {@link recoder.java.JavaProgramElement} are abstract classes defining - standard implementations that already know their - {@link recoder.java.JavaProgramFactory}. -

-

-

Validation
-
- Calling the {@link recoder.ModelElement#validate()} method of a - {@link recoder.ModelElement} will check its consistency similar to the - analysis a compiler does. In case of an inconsistency, a - {@link recoder.ModelException} is thrown. The - {@link recoder.ModelElement#validate()} method of a - {@link recoder.java.ProgramElement} will check its children if - necessary. Calling {@link recoder.ModelElement#validate()} for a - {@link recoder.java.CompilationUnit} will check the consistency of the - whole module. -

- A {@link recoder.java.NonTerminalProgramElement} defines a - {@link recoder.java.NonTerminalProgramElement#makeParentRoleValid()} method - that sets all parent links of the current children. Not that a - {@link recoder.java.SourceElement} automatically keeps track of any attached - {@link recoder.java.Comment}. - The method is automatically invoked by each constructor that creates a - concrete and valid program element. Since some constructors create - partially initialized nodes only, there is no need to make them valid at - that time. -

-

-

Expressions and Statements
-
- {@link recoder.java.Expression} and {@link recoder.java.Statement} are - self-explanatory. A {@link recoder.java.LoopInitializer} is a special - {@link recoder.java.Statement} valid as initializer of - {@link recoder.java.statement.For} loops. - {@link recoder.java.LoopInitializer} is subtyped by - {@link recoder.java.expression.ExpressionStatement} and - {@link recoder.java.declaration.LocalVariableDeclaration}). -

- Concrete classes and further abstractions are bundled in the - {@link recoder.java.expression} and {@link recoder.java.statement} packages. -

-

-

Syntax Tree Parents
-
- There are a couple of abstractions dealing with properties of being a - parent node, which is used for upwards traversals in the syntax tree. -

- These are {@link recoder.java.declaration.TypeDeclarationContainer}, - {@link recoder.java.ExpressionContainer}, - {@link recoder.java.StatementContainer}, - {@link recoder.java.ParameterContainer}, - {@link recoder.java.NamedProgramElement} and - {@link recoder.java.reference.TypeReferenceContainer}. A - An {@link recoder.java.ExpressionContainer} contains - {@link recoder.java.Expression}s, a - {@link recoder.java.StatementContainer} contains - {@link recoder.java.Statement}s, a - {@link recoder.java.ParameterContainer} - (either a {@link recoder.java.declaration.MethodDeclaration} or a - {@link recoder.java.statement.Catch} statement) contains - {@link recoder.java.declaration.ParameterDeclaration}s. - A {@link recoder.java.NamedProgramElement} is a subtype of - {@link recoder.NamedModelElement}. - A {@link recoder.java.reference.TypeReferenceContainer} contains one or - several names, but these are names of types that are referred to explicitely - by a {@link recoder.java.reference.TypeReference}. -

-

-

References
-
- A {@link recoder.java.Reference} is an explicite use of an entity. Most of - these {@link recoder.java.Reference}s are - {@link recoder.java.reference.NameReference}s - and as such {@link recoder.java.NamedProgramElement}s, e.g. the - {@link recoder.java.reference.TypeReference}. - Subtypes of {@link recoder.java.Reference}s are bundled in the - {@link recoder.java.reference} package. -
-

-

Modifiers and Declarations
-
- {@link recoder.java.declaration.Modifier}s are (exclusively) used in the - context of {@link recoder.java.Declaration}s. - {@link recoder.java.declaration.Modifier}s occur explictely, since they occur - as syntactical tokens that might be indented and commented. - {@link recoder.java.Declaration}s are either - declarations of types or other entities such as - {@link recoder.java.declaration.MemberDeclaration} or - {@link recoder.java.declaration.VariableDeclaration}. Concrete - {@link recoder.java.declaration.Modifier}s and - {@link recoder.java.Declaration}s are - bundled in the {@link recoder.java.declaration.modifier} and - {@link recoder.java.declaration} packages. -
-

-

Comments
-
- A {@link recoder.java.ProgramElement} can have a list of - {@link recoder.java.Comment}s attached. -

- While a pure {@link recoder.java.Comment} can extend to several lines, a - {@link recoder.java.SingleLineComment} may not contain linefeeds. - A {@link recoder.java.DocComment} is a special comment used for - documentation systems such as JavaDoc or DOC++. -

-
- diff --git a/recoder/src/main/java/recoder/java/reference/package-info.java b/recoder/src/main/java/recoder/java/reference/package-info.java new file mode 100644 index 00000000000..e6e28b2b92f --- /dev/null +++ b/recoder/src/main/java/recoder/java/reference/package-info.java @@ -0,0 +1,5 @@ +/** + * Elements of the Java syntax tree representing implicit or explicit (named) + * references to other program elements. + */ +package recoder.java.reference; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/reference/package.html b/recoder/src/main/java/recoder/java/reference/package.html deleted file mode 100644 index 552721738c8..00000000000 --- a/recoder/src/main/java/recoder/java/reference/package.html +++ /dev/null @@ -1,4 +0,0 @@ - -Elements of the Java syntax tree representing implicit or explicit (named) -references to other program elements. - diff --git a/recoder/src/main/java/recoder/java/statement/package-info.java b/recoder/src/main/java/recoder/java/statement/package-info.java new file mode 100644 index 00000000000..02f3e72f3f3 --- /dev/null +++ b/recoder/src/main/java/recoder/java/statement/package-info.java @@ -0,0 +1,6 @@ +/** + * Elements of the Java syntax tree representing pure statements. + * Besides these other valid statements are the various expressions with + * side effects ({@link recoder.java.expression.ExpressionStatement}s). + */ +package recoder.java.statement; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/java/statement/package.html b/recoder/src/main/java/recoder/java/statement/package.html deleted file mode 100644 index 03389525545..00000000000 --- a/recoder/src/main/java/recoder/java/statement/package.html +++ /dev/null @@ -1,5 +0,0 @@ - -Elements of the Java syntax tree representing pure statements. -Besides these other valid statements are the various expressions with -side effects ({@link recoder.java.expression.ExpressionStatement}s). - diff --git a/recoder/src/main/java/recoder/kit/package-info.java b/recoder/src/main/java/recoder/kit/package-info.java new file mode 100644 index 00000000000..8fc4ce19ab4 --- /dev/null +++ b/recoder/src/main/java/recoder/kit/package-info.java @@ -0,0 +1,9 @@ +/** + * This package contains the RECODER transformation framework. + * The auxiliary "kit" classes contain queries and factory methods, + * while high level transformations are subclasses of + * {@link recoder.kit.Transformation}. Transformations report + * possible problems; specialized problem reports are collected + * in the {@link recoder.kit.transformation} package. + */ +package recoder.kit; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/kit/package.html b/recoder/src/main/java/recoder/kit/package.html deleted file mode 100644 index ad2af3f9442..00000000000 --- a/recoder/src/main/java/recoder/kit/package.html +++ /dev/null @@ -1,8 +0,0 @@ - -This package contains the RECODER transformation framework. -The auxiliary "kit" classes contain queries and factory methods, -while high level transformations are subclasses of -{@link recoder.kit.Transformation}. Transformations report -possible problems; specialized problem reports are collected -in the {@link recoder.kit.transformation} package. - diff --git a/recoder/src/main/java/recoder/kit/pattern/package-info.java b/recoder/src/main/java/recoder/kit/pattern/package-info.java new file mode 100644 index 00000000000..a2059e61800 --- /dev/null +++ b/recoder/src/main/java/recoder/kit/pattern/package-info.java @@ -0,0 +1,10 @@ +/** + * This package contains classes that model design patterns; it is far from + * being stable and will be subject to changes. + *

+ * Each instance of a pattern knows its participants and serves as an entry + * of a pattern repository. In addition, pattern classes provide means to + * generate certain pattern implementations and can check parts of their + * contracts. + */ +package recoder.kit.pattern; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/kit/pattern/package.html b/recoder/src/main/java/recoder/kit/pattern/package.html deleted file mode 100644 index c4cab1550a3..00000000000 --- a/recoder/src/main/java/recoder/kit/pattern/package.html +++ /dev/null @@ -1,9 +0,0 @@ - -This package contains classes that model design patterns; it is far from -being stable and will be subject to changes. -

- Each instance of a pattern knows its participants and serves as an entry - of a pattern repository. In addition, pattern classes provide means to - generate certain pattern implementations and can check parts of their - contracts. - diff --git a/recoder/src/main/java/recoder/kit/transformation/package-info.java b/recoder/src/main/java/recoder/kit/transformation/package-info.java new file mode 100644 index 00000000000..5b4929cf885 --- /dev/null +++ b/recoder/src/main/java/recoder/kit/transformation/package-info.java @@ -0,0 +1,5 @@ +/** + * This package contains transformation command objects and + * associated problem reports. + */ +package recoder.kit.transformation; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/kit/transformation/package.html b/recoder/src/main/java/recoder/kit/transformation/package.html deleted file mode 100644 index 5d5811d6916..00000000000 --- a/recoder/src/main/java/recoder/kit/transformation/package.html +++ /dev/null @@ -1,4 +0,0 @@ - -This package contains transformation command objects and -associated problem reports. - diff --git a/recoder/src/main/java/recoder/list/package-info.java b/recoder/src/main/java/recoder/list/package-info.java new file mode 100644 index 00000000000..0df7a945a25 --- /dev/null +++ b/recoder/src/main/java/recoder/list/package-info.java @@ -0,0 +1,43 @@ +/** + * This package containes generated list and iterator types. + *

+ *
Implementation
+ *
+ * The elements are addressed by indices rather than iterators or + * explicite nodes. This saves storage and provides a slim interface. + *

+ * The default implementations end with "ArrayList" and use the common + * array doubling technique. + * If elements must be added and the number is known a-priori (e.g. before + * concatenating a set of lists), it is wise to increase the capacity of the + * array with {@link recoder.list.ObjectArrayList#ensureCapacity}. + *

+ *
Genericity
+ *
+ * The lists are heterogeneous emulations of generic classes. + * Specialized versions inherit from {@link recoder.list.ObjectList} and delegate + * to the "untyped" (i.e. Object type) methods. Since the untyped + * methods are not public in {@link recoder.list.ObjectList}, this is quite safe. + *
+ *
Mutability
+ *
+ * The standard list interfaces are read-only. To modify a list, one must + * use a XYZMutableList that extends the corresponding XYZList interface. + *

+ * The read-only List interfaces are additionally inherited in parallel to + * the relations between the element types: A {@link recoder.list.ModifierList} + * extends a {@link recoder.list.ProgramElementList} which in turn extends an + * {@link recoder.list.ModelElementList} which extends the + * {@link recoder.list.ObjectList}. With this technique, it is possible + * to add a {@link recoder.list.ModifierList} to a + * {@link recoder.list.ProgramElementMutableList} + * (the {@link recoder.list.ObjectArrayList#add} method expects a + * {@link recoder.list.ProgramElementList} which is a proper superclass of + * {@link recoder.list.ModifierList}). + * Note that to avoid covariance problems (i.e. the preconditions of e.g. + * add methods are not in a sense compatible in polymorphic contexts), the + * mutable lists are not inherited from each other. + *

+ *
+ */ +package recoder.list; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/list/package.html b/recoder/src/main/java/recoder/list/package.html deleted file mode 100644 index 8e7089afa61..00000000000 --- a/recoder/src/main/java/recoder/list/package.html +++ /dev/null @@ -1,43 +0,0 @@ - - -This package containes generated list and iterator types. -
-
Implementation
-
- The elements are addressed by indices rather than iterators or - explicite nodes. This saves storage and provides a slim interface. -

- The default implementations end with "ArrayList" and use the common - array doubling technique. - If elements must be added and the number is known a-priori (e.g. before - concatenating a set of lists), it is wise to increase the capacity of the - array with {@link recoder.list.ObjectArrayList#ensureCapacity}. -

-
Genericity
-
- The lists are heterogeneous emulations of generic classes. - Specialized versions inherit from {@link recoder.list.ObjectList} and delegate - to the "untyped" (i.e. Object type) methods. Since the untyped - methods are not public in {@link recoder.list.ObjectList}, this is quite safe. -
-
Mutability
-
- The standard list interfaces are read-only. To modify a list, one must - use a XYZMutableList that extends the corresponding XYZList interface. -

- The read-only List interfaces are additionally inherited in parallel to - the relations between the element types: A {@link recoder.list.ModifierList} - extends a {@link recoder.list.ProgramElementList} which in turn extends an - {@link recoder.list.ModelElementList} which extends the - {@link recoder.list.ObjectList}. With this technique, it is possible - to add a {@link recoder.list.ModifierList} to a - {@link recoder.list.ProgramElementMutableList} - (the {@link recoder.list.ObjectArrayList#add} method expects a - {@link recoder.list.ProgramElementList} which is a proper superclass of - {@link recoder.list.ModifierList}). - Note that to avoid covariance problems (i.e. the preconditions of e.g. - add methods are not in a sense compatible in polymorphic contexts), the - mutable lists are not inherited from each other. -

-
- \ No newline at end of file diff --git a/recoder/src/main/java/recoder/package-info.java b/recoder/src/main/java/recoder/package-info.java new file mode 100644 index 00000000000..6cc1632a8c6 --- /dev/null +++ b/recoder/src/main/java/recoder/package-info.java @@ -0,0 +1,17 @@ +/** + * This package contains some basic definitions. + *

+ * The central class of the RECODER system is {@link recoder.ServiceConfiguration} + * which is responsible for maintaining all information repositories. A very + * important repository is the {@link recoder.io.SourceFileRepository}, which + * holds the set of known syntax trees. The construction of new syntax elements + * lays in the responsibility of the {@link recoder.ProgramFactory} which also + * allows access to a parser for the given language or language dialect. + * Other repositories may know about additional abstractions or may + * provide results derived by semantical analyses. + *

+ * Besides of the base repositories, the package also contains some base + * abstractions. + * {@link recoder.ModelElement} is the parent of most other classes of the model. + */ +package recoder; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/package.html b/recoder/src/main/java/recoder/package.html deleted file mode 100644 index e9c52eba382..00000000000 --- a/recoder/src/main/java/recoder/package.html +++ /dev/null @@ -1,16 +0,0 @@ - -This package contains some basic definitions. -

- The central class of the RECODER system is {@link recoder.ServiceConfiguration} - which is responsible for maintaining all information repositories. A very - important repository is the {@link recoder.io.SourceFileRepository}, which - holds the set of known syntax trees. The construction of new syntax elements - lays in the responsibility of the {@link recoder.ProgramFactory} which also - allows access to a parser for the given language or language dialect. - Other repositories may know about additional abstractions or may - provide results derived by semantical analyses. -

- Besides of the base repositories, the package also contains some base - abstractions. - {@link recoder.ModelElement} is the parent of most other classes of the model. - diff --git a/recoder/src/main/java/recoder/parser/package-info.java b/recoder/src/main/java/recoder/parser/package-info.java new file mode 100644 index 00000000000..22ef5987d23 --- /dev/null +++ b/recoder/src/main/java/recoder/parser/package-info.java @@ -0,0 +1,6 @@ +/** + * This package contains the JavaCC generated parser. It is not meant + * to be used directly; instead, the {@link recoder.ProgramFactory} defines + * appropriate access methods. + */ +package recoder.parser; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/parser/package.html b/recoder/src/main/java/recoder/parser/package.html deleted file mode 100644 index d44a5b2b2cd..00000000000 --- a/recoder/src/main/java/recoder/parser/package.html +++ /dev/null @@ -1,5 +0,0 @@ - -This package contains the JavaCC generated parser. It is not meant -to be used directly; instead, the {@link recoder.ProgramFactory} defines -appropriate access methods. - diff --git a/recoder/src/main/java/recoder/service/package-info.java b/recoder/src/main/java/recoder/service/package-info.java new file mode 100644 index 00000000000..af9aca3d0bc --- /dev/null +++ b/recoder/src/main/java/recoder/service/package-info.java @@ -0,0 +1,4 @@ +/** + * This package contains the semantical services of RECODER. + */ +package recoder.service; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/service/package.html b/recoder/src/main/java/recoder/service/package.html deleted file mode 100644 index d53b83ff206..00000000000 --- a/recoder/src/main/java/recoder/service/package.html +++ /dev/null @@ -1,3 +0,0 @@ - -This package contains the semantical services of RECODER. - diff --git a/recoder/src/main/java/recoder/util/package-info.java b/recoder/src/main/java/recoder/util/package-info.java new file mode 100644 index 00000000000..4d83b9b12f8 --- /dev/null +++ b/recoder/src/main/java/recoder/util/package-info.java @@ -0,0 +1,8 @@ +/** + * This package provides basic data types and algorithms. + * The equality and order relations are materialized to allow for multiple + * variants instead of one fixed version. For instance, it is possible + * to create a hash table that uses object identity, the fixed "natural" + * hash codes, or any other version. + */ +package recoder.util; \ No newline at end of file diff --git a/recoder/src/main/java/recoder/util/package.html b/recoder/src/main/java/recoder/util/package.html deleted file mode 100644 index 8e417d91eb6..00000000000 --- a/recoder/src/main/java/recoder/util/package.html +++ /dev/null @@ -1,7 +0,0 @@ - -This package provides basic data types and algorithms. -The equality and order relations are materialized to allow for multiple -variants instead of one fixed version. For instance, it is possible -to create a hash table that uses object identity, the fixed "natural" -hash codes, or any other version. - diff --git a/recoder/src/test/resources/java5/src/transformations/util/package-info.java b/recoder/src/test/resources/java5/src/transformations/util/package-info.java new file mode 100644 index 00000000000..b19cecd47c9 --- /dev/null +++ b/recoder/src/test/resources/java5/src/transformations/util/package-info.java @@ -0,0 +1,8 @@ +/** + * This package provides basic data types and algorithms. + * The equality and order relations are materialized to allow for multiple + * variants instead of one fixed version. For instance, it is possible + * to create a hash table that uses object identity, the fixed "natural" + * hash codes, or any other version. + */ +package java5.src.transformations.util; \ No newline at end of file diff --git a/recoder/src/test/resources/java5/src/transformations/util/package.html b/recoder/src/test/resources/java5/src/transformations/util/package.html deleted file mode 100644 index 8e417d91eb6..00000000000 --- a/recoder/src/test/resources/java5/src/transformations/util/package.html +++ /dev/null @@ -1,7 +0,0 @@ - -This package provides basic data types and algorithms. -The equality and order relations are materialized to allow for multiple -variants instead of one fixed version. For instance, it is possible -to create a hash table that uses object identity, the fixed "natural" -hash codes, or any other version. - From 122166779fcd75f31cc4f799cea8386e28c9b39a Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 29 Dec 2023 18:40:07 +0100 Subject: [PATCH 2/2] spotless reformat --- .../uka/ilkd/key/util/rifl/package-info.java | 2 +- .../key/java/abstraction/package-info.java | 2 +- .../declaration/modifier/package-info.java | 2 +- .../key/java/declaration/package-info.java | 2 +- .../java/expression/literal/package-info.java | 2 +- .../expression/operator/package-info.java | 2 +- .../key/java/expression/package-info.java | 2 +- .../de/uka/ilkd/key/java/package-info.java | 12 +++++---- .../key/java/recoderext/adt/package-info.java | 8 +++--- .../ilkd/key/java/reference/package-info.java | 2 +- .../ilkd/key/java/statement/package-info.java | 2 +- .../ilkd/key/java/visitor/package-info.java | 2 +- .../de/uka/ilkd/key/ldt/package-info.java | 2 +- .../uka/ilkd/key/logic/op/package-info.java | 2 +- .../de/uka/ilkd/key/logic/package-info.java | 25 ++++++++++++------- .../uka/ilkd/key/logic/sort/package-info.java | 2 +- .../java/de/uka/ilkd/key/pp/package-info.java | 2 +- .../uka/ilkd/key/proof/init/package-info.java | 2 +- .../uka/ilkd/key/proof/io/package-info.java | 2 +- .../uka/ilkd/key/proof/mgt/package-info.java | 2 +- .../de/uka/ilkd/key/proof/package-info.java | 2 +- .../uka/ilkd/key/rule/inst/package-info.java | 2 +- .../metaconstruct/arith/package-info.java | 4 +-- .../key/rule/metaconstruct/package-info.java | 4 +-- .../de/uka/ilkd/key/rule/package-info.java | 2 +- .../de/uka/ilkd/key/smt/package-info.java | 2 +- .../uka/ilkd/key/speclang/package-info.java | 2 +- .../uka/ilkd/key/strategy/package-info.java | 2 +- .../de/uka/ilkd/key/util/package-info.java | 2 +- .../de/uka/ilkd/key/util/pp/package-info.java | 24 +++++++++++------- .../key/gui/configuration/package-info.java | 2 +- .../de/uka/ilkd/key/gui/package-info.java | 2 +- .../de/uka/ilkd/key/gui/smt/package-info.java | 2 +- .../recoder/abstraction/package-info.java | 2 +- .../java/recoder/bytecode/package-info.java | 2 +- .../recoder/convenience/package-info.java | 2 +- .../main/java/recoder/io/package-info.java | 2 +- .../declaration/modifier/package-info.java | 2 +- .../java/declaration/package-info.java | 2 +- .../java/expression/literal/package-info.java | 2 +- .../expression/operator/package-info.java | 2 +- .../recoder/java/expression/package-info.java | 2 +- .../main/java/recoder/java/package-info.java | 2 +- .../recoder/java/reference/package-info.java | 2 +- .../recoder/java/statement/package-info.java | 2 +- .../main/java/recoder/kit/package-info.java | 2 +- .../recoder/kit/pattern/package-info.java | 2 +- .../kit/transformation/package-info.java | 2 +- .../main/java/recoder/list/package-info.java | 2 +- .../src/main/java/recoder/package-info.java | 2 +- .../java/recoder/parser/package-info.java | 2 +- .../java/recoder/service/package-info.java | 2 +- .../main/java/recoder/util/package-info.java | 2 +- 53 files changed, 94 insertions(+), 77 deletions(-) diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java index 7420b91e7b5..49bbd163229 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java @@ -5,4 +5,4 @@ * 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; \ No newline at end of file +package de.uka.ilkd.key.util.rifl; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java index a6097492143..a41fd6023cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java @@ -16,4 +16,4 @@ * {@link recoder.service.SourceInfo} implementations and should * not be modified from others. */ -package de.uka.ilkd.key.java.abstraction; \ No newline at end of file +package de.uka.ilkd.key.java.abstraction; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java index 0d1cddbc5cd..573a2c02dcc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java @@ -3,4 +3,4 @@ * the parent {@link recoder.java.declaration.Modifier} is the * {@link recoder.java.declaration.modifier.VisibilityModifier}. */ -package de.uka.ilkd.key.java.declaration.modifier; \ No newline at end of file +package de.uka.ilkd.key.java.declaration.modifier; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java index d7764b669e9..4e9c501b3db 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java @@ -8,4 +8,4 @@ * The modifiers themselves are collected in the subpackage * {@link recoder.java.declaration.modifier}. */ -package de.uka.ilkd.key.java.declaration; \ No newline at end of file +package de.uka.ilkd.key.java.declaration; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java index 1a2c375c966..6f573f83202 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java @@ -4,4 +4,4 @@ * {@link recoder.java.expression.literal.NullLiteral} and * {@link recoder.java.expression.literal.StringLiteral}. */ -package de.uka.ilkd.key.java.expression.literal; \ No newline at end of file +package de.uka.ilkd.key.java.expression.literal; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java index 583fd4cbc12..e17b09bf1e5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java @@ -4,4 +4,4 @@ * {@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; \ No newline at end of file +package de.uka.ilkd.key.java.expression.operator; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java index ee80e567e01..67fcd0d116d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java @@ -3,4 +3,4 @@ * The various operators and literals are bundled in the corresponding * subpackages. */ -package de.uka.ilkd.key.java.expression; \ No newline at end of file +package de.uka.ilkd.key.java.expression; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java index 5ae7d044d74..800a5af5b50 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/package-info.java @@ -12,7 +12,8 @@ *

Source and Program Elements
*
* 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}. + * necessary a {@link de.uka.ilkd.key.java.ModelElement}, such as a + * {@link de.uka.ilkd.key.java.Comment}. *

* 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 @@ -21,7 +22,8 @@ *

* {@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} + * {@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}. @@ -56,7 +58,7 @@ * {@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 + * {@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 @@ -92,7 +94,7 @@ * {@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.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 @@ -100,4 +102,4 @@ *

* */ -package de.uka.ilkd.key.java; \ No newline at end of file +package de.uka.ilkd.key.java; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java index 2a28f741f15..4ee9164bded 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java @@ -1,5 +1,7 @@ /** - * This package contains RecodeR Operators - * which represent algebraic data type functions. (See also the ldt package description.) + * This package contains RecodeR Operators + * which represent algebraic data type functions. (See also the + * ldt package description.) */ -package de.uka.ilkd.key.java.recoderext.adt; \ No newline at end of file +package de.uka.ilkd.key.java.recoderext.adt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java index 3d8cb9af65c..7837159e931 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/package-info.java @@ -2,4 +2,4 @@ * Elements of the Java syntax tree representing implicit or explicit (named) * references to other program elements. */ -package de.uka.ilkd.key.java.reference; \ No newline at end of file +package de.uka.ilkd.key.java.reference; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java index 673dd6ba5e9..c05a5d19b7e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/package-info.java @@ -3,4 +3,4 @@ * Besides these other valid statements are the various expressions with * side effects ({@link recoder.java.expression.ExpressionStatement}s). */ -package de.uka.ilkd.key.java.statement; \ No newline at end of file +package de.uka.ilkd.key.java.statement; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java index 40c024d906f..5e3aa139acc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/package-info.java @@ -2,4 +2,4 @@ * contains classes representing visitors traversing the tree * structure of Java programs. */ -package de.uka.ilkd.key.java.visitor; \ No newline at end of file +package de.uka.ilkd.key.java.visitor; diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java index c009262e6c5..4edf3521570 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java @@ -4,4 +4,4 @@ * programming interface to access the entities declared in these * rule files. */ -package de.uka.ilkd.key.ldt; \ No newline at end of file +package de.uka.ilkd.key.ldt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java index 2d10005e5e6..7bbf6a3358e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/package-info.java @@ -17,4 +17,4 @@ * de.uka.ilkd.key.logic.op.SchemaVariable}s for {@link * de.uka.ilkd.key.rule.Taclet}s. */ -package de.uka.ilkd.key.logic.op; \ No newline at end of file +package de.uka.ilkd.key.logic.op; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java index b0ab26c0d33..6b837c99a90 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/package-info.java @@ -1,5 +1,6 @@ /** - *

provides a representation for the term and sequent + *

+ * provides a representation for the term and sequent * structure. The structure of a term is defined in {@link * de.uka.ilkd.key.logic.Term}. Subclasses of {@link * de.uka.ilkd.key.logic.Term} provide representations for special @@ -9,26 +10,32 @@ * subclasses. Moreover, {@link de.uka.ilkd.key.logic.Term}s (or * their subclasses) are supposed to be never constructed by * constructors of their own, but by instances of {@link - * de.uka.ilkd.key.logic.TermFactory}.

- *

The function of {@link de.uka.ilkd.key.logic.Term}s (e.g., if + * de.uka.ilkd.key.logic.TermFactory}. + *

+ *

+ * The function of {@link de.uka.ilkd.key.logic.Term}s (e.g., if * they represent a conjunction of subterms, a quantified * formula,...) is only determined by an {@link * de.uka.ilkd.key.logic.op.Operator} that is assigned to a {@link * de.uka.ilkd.key.logic.Term} when the {@link - * de.uka.ilkd.key.logic.Term} is constructed.

- *

{@link de.uka.ilkd.key.logic.Sequent}s consist of two {@link + * de.uka.ilkd.key.logic.Term} is constructed. + *

+ *

+ * {@link de.uka.ilkd.key.logic.Sequent}s consist of two {@link * de.uka.ilkd.key.logic.Semisequent}s which represent a * duplicate-free list of a {@link * de.uka.ilkd.key.logic.SequentFormula}s. The latter consist of * a {@link de.uka.ilkd.key.logic.Constraint} and a {@link * de.uka.ilkd.key.logic.Term} of a special sort {@link - * de.uka.ilkd.key.logic.sort.Sort#FORMULA}.

- *

{@link de.uka.ilkd.key.logic.Sequent}s and {@link + * de.uka.ilkd.key.logic.sort.Sort#FORMULA}. + *

+ *

+ * {@link de.uka.ilkd.key.logic.Sequent}s and {@link * de.uka.ilkd.key.logic.Term}s are immutable. *

* * - * Last modified: Wed Dec 4 15:11:14 MET 2002 + * Last modified: Wed Dec 4 15:11:14 MET 2002 * */ -package de.uka.ilkd.key.logic; \ No newline at end of file +package de.uka.ilkd.key.logic; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java index 5511d09c41d..a4ff0146683 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/package-info.java @@ -7,4 +7,4 @@ * In KeY we distinguish formulas from terms by the special sort instance * Sort.Formula. */ -package de.uka.ilkd.key.logic.sort; \ No newline at end of file +package de.uka.ilkd.key.logic.sort; diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java index 8cd2b762bbd..8cfd6eb1853 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/package-info.java @@ -2,4 +2,4 @@ * This package contains pretty-printing functionality used by the GUI and for * saving proofs. */ -package de.uka.ilkd.key.pp; \ No newline at end of file +package de.uka.ilkd.key.pp; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java index 414abffbb7a..fa3f28aca24 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/package-info.java @@ -4,4 +4,4 @@ * EnvInput (provides a proof environment) and ProofOblInput (provides one or many * sequents whose validity is to be proven). */ -package de.uka.ilkd.key.proof.init; \ No newline at end of file +package de.uka.ilkd.key.proof.init; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java index 1276060d13b..e558a3a92c0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/package-info.java @@ -1,4 +1,4 @@ /** * Classes related to loading and saving proof files. */ -package de.uka.ilkd.key.proof.io; \ No newline at end of file +package de.uka.ilkd.key.proof.io; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java index 94a92e3a217..400e8b62266 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java @@ -3,4 +3,4 @@ * example, proof management ensures that contract applications cannot lead to * unsound cyclic dependencies between proofs. */ -package de.uka.ilkd.key.proof.mgt; \ No newline at end of file +package de.uka.ilkd.key.proof.mgt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java index bbcf3c62f5a..84a5861d0b6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/package-info.java @@ -2,4 +2,4 @@ * This package contains the core data structures of proofs, nodes, goals, as well * as machinery to deal with these data structures. */ -package de.uka.ilkd.key.proof; \ No newline at end of file +package de.uka.ilkd.key.proof; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java index 1a0ec2117a2..2303f184f32 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/package-info.java @@ -2,4 +2,4 @@ * contains classes for the instantiation of schema variables of {@link * de.uka.ilkd.key.rule.Taclet}s. */ -package de.uka.ilkd.key.rule.inst; \ No newline at end of file +package de.uka.ilkd.key.rule.inst; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java index a13bae15f8f..8c549dbd760 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/package-info.java @@ -1,5 +1,5 @@ /** - * contains classes representing the special meta constructs of {@link + * contains classes representing the special meta constructs of {@link * de.uka.ilkd.key.rule.Taclet}s performing arithmetic operations. */ -package de.uka.ilkd.key.rule.metaconstruct.arith; \ No newline at end of file +package de.uka.ilkd.key.rule.metaconstruct.arith; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java index 753f96f9e56..c908c6a846d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/package-info.java @@ -1,5 +1,5 @@ /** - * contains classes representing the meta constructs of {@link + * contains classes representing the meta constructs of {@link * de.uka.ilkd.key.rule.Taclet}s. */ -package de.uka.ilkd.key.rule.metaconstruct; \ No newline at end of file +package de.uka.ilkd.key.rule.metaconstruct; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java index 6e7df2eb20e..f4f0fa03e57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/package-info.java @@ -7,4 +7,4 @@ * de.uka.ilkd.key.rule.TacletBuilder}). Besides taclets, there are * built-in rules implemented directly in Java. */ -package de.uka.ilkd.key.rule; \ No newline at end of file +package de.uka.ilkd.key.rule; diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java index 5d7738b7b01..563f1bde8a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/package-info.java @@ -3,4 +3,4 @@ * to formulas in formats such as SMT-LIB, and allowing to send such formulas to * SMT solvers such as Simplify or Z3. */ -package de.uka.ilkd.key.smt; \ No newline at end of file +package de.uka.ilkd.key.smt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java index 86674f87011..817a632f015 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/package-info.java @@ -5,4 +5,4 @@ * OperationContract, and DependencyContract. These are used as input by the * proof obligations declared in package proof.init. */ -package de.uka.ilkd.key.speclang; \ No newline at end of file +package de.uka.ilkd.key.speclang; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java index 93c5d20544c..3687946ff8a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/package-info.java @@ -1,4 +1,4 @@ /** * This package contains classes implementing the proof search strategies of KeY. */ -package de.uka.ilkd.key.strategy; \ No newline at end of file +package de.uka.ilkd.key.strategy; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java index 6ca9c1ca0ac..0ce8a09b6c4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java @@ -3,4 +3,4 @@ * side functionalities like the installer (subpackage install), and the tool for * removing generics from a Java program (subpackage removegenerics). */ -package de.uka.ilkd.key.util; \ No newline at end of file +package de.uka.ilkd.key.util; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java index ac450158480..7362fb0d6ca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/pp/package-info.java @@ -1,20 +1,26 @@ /** * A package to pretty-print information using line breaks and - * indentation. For instance, it can be used to print + * indentation. For instance, it can be used to print + * * 

- * while (i>0) {
- * i--;
- * j++;
+ * while (i > 0) {
+ *     i--;
+ *     j++;
  * }
  *
+ * * instead of + * * 
- * while (i>0) { i
- * --; j++;}
+ * while (i > 0) {
+ *     i--;
+ *     j++;
+ * }
  *
- * if a maximum line width of 15 characters is chosen. The frontend + * + * if a maximum line width of 15 characters is chosen. The frontend * to the Pretty-Printer is the {@link - * de.uka.ilkd.key.util.pp.Layouter} class. You may configure what + * de.uka.ilkd.key.util.pp.Layouter} class. You may configure what * happens with the output by implemenenting the {@link * de.uka.ilkd.key.util.pp.Backend} interface, or by using the * standard implementation {@link @@ -22,4 +28,4 @@ * * @author Martin Giese */ -package de.uka.ilkd.key.util.pp; \ No newline at end of file +package de.uka.ilkd.key.util.pp; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java index 3e6b71238db..fc954e31693 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/package-info.java @@ -1,4 +1,4 @@ /** * This package contains classes to do with the configuration / settings of KeY. */ -package de.uka.ilkd.key.gui.configuration; \ No newline at end of file +package de.uka.ilkd.key.gui.configuration; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java index 9a0f762150f..0b1a6c5be11 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/package-info.java @@ -1,4 +1,4 @@ /** * This package contains classes forming the graphical user interface of KeY. */ -package de.uka.ilkd.key.gui; \ No newline at end of file +package de.uka.ilkd.key.gui; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java index e9af4b204b1..c235bf20f15 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/package-info.java @@ -1,4 +1,4 @@ /** * This package contains the graphical user interface of the SMT backend. */ -package de.uka.ilkd.key.gui.smt; \ No newline at end of file +package de.uka.ilkd.key.gui.smt; diff --git a/recoder/src/main/java/recoder/abstraction/package-info.java b/recoder/src/main/java/recoder/abstraction/package-info.java index e6735125ac2..fb91fe0c4a4 100644 --- a/recoder/src/main/java/recoder/abstraction/package-info.java +++ b/recoder/src/main/java/recoder/abstraction/package-info.java @@ -15,4 +15,4 @@ * {@link recoder.service.SourceInfo} implementations; the corresponding * methods should not be uses by others. */ -package recoder.abstraction; \ No newline at end of file +package recoder.abstraction; diff --git a/recoder/src/main/java/recoder/bytecode/package-info.java b/recoder/src/main/java/recoder/bytecode/package-info.java index b1c78d78859..77ca48f1b02 100644 --- a/recoder/src/main/java/recoder/bytecode/package-info.java +++ b/recoder/src/main/java/recoder/bytecode/package-info.java @@ -3,4 +3,4 @@ * code. As RECODER does not rewrite Bytecode, the information remains on * interface level - no statements are analyzed. */ -package recoder.bytecode; \ No newline at end of file +package recoder.bytecode; diff --git a/recoder/src/main/java/recoder/convenience/package-info.java b/recoder/src/main/java/recoder/convenience/package-info.java index af9b49f1123..ce21961fb12 100644 --- a/recoder/src/main/java/recoder/convenience/package-info.java +++ b/recoder/src/main/java/recoder/convenience/package-info.java @@ -9,4 +9,4 @@ * artificial names. * */ -package recoder.convenience; \ No newline at end of file +package recoder.convenience; diff --git a/recoder/src/main/java/recoder/io/package-info.java b/recoder/src/main/java/recoder/io/package-info.java index 98e7604ae82..1bd2a975cd9 100644 --- a/recoder/src/main/java/recoder/io/package-info.java +++ b/recoder/src/main/java/recoder/io/package-info.java @@ -3,4 +3,4 @@ * The abstractions hide where the information stems from or should go to, * e.g. files with various file formats, databases or graphical interfaces. */ -package recoder.io; \ No newline at end of file +package recoder.io; diff --git a/recoder/src/main/java/recoder/java/declaration/modifier/package-info.java b/recoder/src/main/java/recoder/java/declaration/modifier/package-info.java index ce1ef2e01d7..8e17fc424c0 100644 --- a/recoder/src/main/java/recoder/java/declaration/modifier/package-info.java +++ b/recoder/src/main/java/recoder/java/declaration/modifier/package-info.java @@ -3,4 +3,4 @@ * the parent {@link recoder.java.declaration.Modifier} is the * {@link recoder.java.declaration.modifier.VisibilityModifier}. */ -package recoder.java.declaration.modifier; \ No newline at end of file +package recoder.java.declaration.modifier; diff --git a/recoder/src/main/java/recoder/java/declaration/package-info.java b/recoder/src/main/java/recoder/java/declaration/package-info.java index d64a7973b16..79798178f16 100644 --- a/recoder/src/main/java/recoder/java/declaration/package-info.java +++ b/recoder/src/main/java/recoder/java/declaration/package-info.java @@ -8,4 +8,4 @@ * The modifiers themselves are collected in the subpackage * {@link recoder.java.declaration.modifier}. */ -package recoder.java.declaration; \ No newline at end of file +package recoder.java.declaration; diff --git a/recoder/src/main/java/recoder/java/expression/literal/package-info.java b/recoder/src/main/java/recoder/java/expression/literal/package-info.java index c87f527e517..b61f5aa36fb 100644 --- a/recoder/src/main/java/recoder/java/expression/literal/package-info.java +++ b/recoder/src/main/java/recoder/java/expression/literal/package-info.java @@ -4,4 +4,4 @@ * {@link recoder.java.expression.literal.NullLiteral} and * {@link recoder.java.expression.literal.StringLiteral}. */ -package recoder.java.expression.literal; \ No newline at end of file +package recoder.java.expression.literal; diff --git a/recoder/src/main/java/recoder/java/expression/operator/package-info.java b/recoder/src/main/java/recoder/java/expression/operator/package-info.java index 13d009834f9..14a4eec19c9 100644 --- a/recoder/src/main/java/recoder/java/expression/operator/package-info.java +++ b/recoder/src/main/java/recoder/java/expression/operator/package-info.java @@ -4,4 +4,4 @@ * {@link recoder.java.expression.operator.New} is also considered an * operator ({@link recoder.java.expression.operator.TypeOperator}). */ -package recoder.java.expression.operator; \ No newline at end of file +package recoder.java.expression.operator; diff --git a/recoder/src/main/java/recoder/java/expression/package-info.java b/recoder/src/main/java/recoder/java/expression/package-info.java index 6e426b0b81c..294b05e2084 100644 --- a/recoder/src/main/java/recoder/java/expression/package-info.java +++ b/recoder/src/main/java/recoder/java/expression/package-info.java @@ -3,4 +3,4 @@ * The various operators and literals are bundled in the corresponding * subpackages. */ -package recoder.java.expression; \ No newline at end of file +package recoder.java.expression; diff --git a/recoder/src/main/java/recoder/java/package-info.java b/recoder/src/main/java/recoder/java/package-info.java index 3dfa4049eab..347300639a9 100644 --- a/recoder/src/main/java/recoder/java/package-info.java +++ b/recoder/src/main/java/recoder/java/package-info.java @@ -132,4 +132,4 @@ * * */ -package recoder.java; \ No newline at end of file +package recoder.java; diff --git a/recoder/src/main/java/recoder/java/reference/package-info.java b/recoder/src/main/java/recoder/java/reference/package-info.java index e6e28b2b92f..c5f707a5929 100644 --- a/recoder/src/main/java/recoder/java/reference/package-info.java +++ b/recoder/src/main/java/recoder/java/reference/package-info.java @@ -2,4 +2,4 @@ * Elements of the Java syntax tree representing implicit or explicit (named) * references to other program elements. */ -package recoder.java.reference; \ No newline at end of file +package recoder.java.reference; diff --git a/recoder/src/main/java/recoder/java/statement/package-info.java b/recoder/src/main/java/recoder/java/statement/package-info.java index 02f3e72f3f3..dc7ff53c313 100644 --- a/recoder/src/main/java/recoder/java/statement/package-info.java +++ b/recoder/src/main/java/recoder/java/statement/package-info.java @@ -3,4 +3,4 @@ * Besides these other valid statements are the various expressions with * side effects ({@link recoder.java.expression.ExpressionStatement}s). */ -package recoder.java.statement; \ No newline at end of file +package recoder.java.statement; diff --git a/recoder/src/main/java/recoder/kit/package-info.java b/recoder/src/main/java/recoder/kit/package-info.java index 8fc4ce19ab4..16bea72feb5 100644 --- a/recoder/src/main/java/recoder/kit/package-info.java +++ b/recoder/src/main/java/recoder/kit/package-info.java @@ -6,4 +6,4 @@ * possible problems; specialized problem reports are collected * in the {@link recoder.kit.transformation} package. */ -package recoder.kit; \ No newline at end of file +package recoder.kit; diff --git a/recoder/src/main/java/recoder/kit/pattern/package-info.java b/recoder/src/main/java/recoder/kit/pattern/package-info.java index a2059e61800..848c156a13f 100644 --- a/recoder/src/main/java/recoder/kit/pattern/package-info.java +++ b/recoder/src/main/java/recoder/kit/pattern/package-info.java @@ -7,4 +7,4 @@ * generate certain pattern implementations and can check parts of their * contracts. */ -package recoder.kit.pattern; \ No newline at end of file +package recoder.kit.pattern; diff --git a/recoder/src/main/java/recoder/kit/transformation/package-info.java b/recoder/src/main/java/recoder/kit/transformation/package-info.java index 5b4929cf885..a4808e30016 100644 --- a/recoder/src/main/java/recoder/kit/transformation/package-info.java +++ b/recoder/src/main/java/recoder/kit/transformation/package-info.java @@ -2,4 +2,4 @@ * This package contains transformation command objects and * associated problem reports. */ -package recoder.kit.transformation; \ No newline at end of file +package recoder.kit.transformation; diff --git a/recoder/src/main/java/recoder/list/package-info.java b/recoder/src/main/java/recoder/list/package-info.java index 0df7a945a25..58e63c5c4c3 100644 --- a/recoder/src/main/java/recoder/list/package-info.java +++ b/recoder/src/main/java/recoder/list/package-info.java @@ -40,4 +40,4 @@ * * */ -package recoder.list; \ No newline at end of file +package recoder.list; diff --git a/recoder/src/main/java/recoder/package-info.java b/recoder/src/main/java/recoder/package-info.java index 6cc1632a8c6..1680ba7f99b 100644 --- a/recoder/src/main/java/recoder/package-info.java +++ b/recoder/src/main/java/recoder/package-info.java @@ -14,4 +14,4 @@ * abstractions. * {@link recoder.ModelElement} is the parent of most other classes of the model. */ -package recoder; \ No newline at end of file +package recoder; diff --git a/recoder/src/main/java/recoder/parser/package-info.java b/recoder/src/main/java/recoder/parser/package-info.java index 22ef5987d23..8e69db2c460 100644 --- a/recoder/src/main/java/recoder/parser/package-info.java +++ b/recoder/src/main/java/recoder/parser/package-info.java @@ -3,4 +3,4 @@ * to be used directly; instead, the {@link recoder.ProgramFactory} defines * appropriate access methods. */ -package recoder.parser; \ No newline at end of file +package recoder.parser; diff --git a/recoder/src/main/java/recoder/service/package-info.java b/recoder/src/main/java/recoder/service/package-info.java index af9aca3d0bc..cbf3e95da24 100644 --- a/recoder/src/main/java/recoder/service/package-info.java +++ b/recoder/src/main/java/recoder/service/package-info.java @@ -1,4 +1,4 @@ /** * This package contains the semantical services of RECODER. */ -package recoder.service; \ No newline at end of file +package recoder.service; diff --git a/recoder/src/main/java/recoder/util/package-info.java b/recoder/src/main/java/recoder/util/package-info.java index 4d83b9b12f8..8ef178503fe 100644 --- a/recoder/src/main/java/recoder/util/package-info.java +++ b/recoder/src/main/java/recoder/util/package-info.java @@ -5,4 +5,4 @@ * to create a hash table that uses object identity, the fixed "natural" * hash codes, or any other version. */ -package recoder.util; \ No newline at end of file +package recoder.util;