Fix all warnings reported by ./gradlew javadoc

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java

@@ -6,7 +6,7 @@
 import java.util.Arrays;
 
 /**
- * Program elements which may be named as sources or sinks in RIFL/Java. Currently fields, method
+ * Program elements which may be named as sources or sinks in RIFL/Java. Currently, fields, method
  * parameters, and method return values can be named both sources and sinks.
  *
  * @author bruns
@@ -138,9 +138,9 @@ public static final class ReturnValue extends SpecificationEntity {
          * Creates a new specification element for a method return.
          *
          * @param m name of the method with parameter types in parentheses
-         * @param pt names of the parameter types of the method
          * @param p package name of the class where the method is declared
          * @param c name of the class where the method is declared
+         * @param t a type
          */
         ReturnValue(String m, String p, String c, Type t) {
             super(p, c, t);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java

@@ -31,6 +31,8 @@
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.CollectionUtil;
 
+// need to switch spotless off for this comment as it replaces @code with @code
+// spotless:off
 /**
  * <p>
  * Instances of this class can be used to compute memory layouts (objects with values and
@@ -41,24 +43,26 @@
  * started. Such memory layouts are named <i>initial memory layouts</i>.
  * </p>
  * <p>
- * Example program:
+ * Example program:<br/>
  *
  * <pre>
- * <code>
- * public class Example {
- *    private int value;
+ * {@code
+ *     public class Example {
+ *         private int value;
  *
- *    private Example next;
+ *         private Example next;
  *
- *    public static int main(Example e) {
- *       e.value = 1;
- *       e.next.value = 2;
- *       return e.value + e.next.value; // Current node in KeY's proof tree
- *    }
+ *         public static int main(Example e) {
+ *             e.value = 1;
+ *             e.next.value = 2;
+ *             return e.value + e.next.value; // Current node in KeY's proof tree
+ *         }
+ *     }
  * }
- * </code>
  * </pre>
  *
+ * </p>
+ * <p>
  * If the symbolic execution stops at the return statement, two memory layouts are possible. In the
  * first case refers {@code e} and {@code e.next} to different objects (result is {@code 3}). In the
  * second case refers both to the same object (result is {@code 4}). That both objects can't be
@@ -68,15 +72,15 @@
  * The following code snippet shows how to use this class:
  *
  * <pre>
- * <code>
- * SymbolicLayoutExtractor e = new SymbolicLayoutExtractor(node);
- * e.analyse();
- * for (int i = 0; i < e.getLayoutsCount(); i++) {
- *    ImmutableList&lt;ISymbolicEquivalenceClass&gt; equivalenceClasses = e.getEquivalenceClasses(i);
- *    ISymbolicLayout initial = e.getInitialLayout(i);
- *    ISymbolicLayout current = e.getCurrentLayout(i);
+ * {@code
+ *     SymbolicLayoutExtractor e = new SymbolicLayoutExtractor(node);
+ *     e.analyse();
+ *     for (int i = 0; i < e.getLayoutsCount(); i++) {
+ *         ImmutableList&lt;ISymbolicEquivalenceClass&gt; equivalenceClasses = e.getEquivalenceClasses(i);
+ *         ISymbolicLayout initial = e.getInitialLayout(i);
+ *         ISymbolicLayout current = e.getCurrentLayout(i);
+ *     }
  * }
- * </code>
  * </pre>
  * </p>
  * <p>
@@ -128,6 +132,7 @@
  * @see ISymbolicLayout
  * @see ExecutionNodeSymbolicLayoutExtractor
  */
+// spotless:on
 public class SymbolicLayoutExtractor extends AbstractUpdateExtractor {
     /**
      * The used {@link IModelSettings}.

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java

@@ -42,17 +42,22 @@
  * The generated {@link Sequent} has the following form:
  *
  * <pre>
- * <code>
+ * {@code
  * ==>
- * &lt;generalAssumptions&gt; &
- * &lt;preconditions&gt;
+ * <generalAssumptions> &
+ * <preconditions>
  * ->
- * &lt;updatesToStoreInitialValues&gt;
- * &lt;modalityStart&gt;
- * exc=null;try {&lt;methodBodyStatement&gt}catch(java.lang.Exception e) {exc = e}
- * &lt;modalityEnd&gt;
- * (exc = null & &lt;postconditions &gt; & &lt;optionalUninterpretedPredicate&gt;)
- * </code>
+ * <updatesToStoreInitialValues>
+ * <modalityStart>
+ * exc=null;
+ * try {
+ *   <methodBodyStatement>
+ * } catch(java.lang.Exception e) {
+ *    exc = e
+ * }
+ * <modalityEnd>
+ *  (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
+ * }
  * </pre>
  * </p>
  *

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java

@@ -26,6 +26,8 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+// need to switch spotless off for this comment as it replaces @code with @code
+// spotless:off
 /**
  * <p>
  * This proof obligation executes selected statements of the body of a given {@link IProgramMethod}.
@@ -38,34 +40,47 @@
  * position of the previous statement is exactly the start position of the following statement.
  * </p>
  * <p>
- * Imagine the following snippet: <code><pre>
- * int x = 1; // from 3/59 to 4/16
- * int y = 2; // from 4/16 to 5/16
- * int z = 3; // from 5/16 to 6/16
- * </pre></code> To execute only the last two statements a user would select intuitively the source
+ * Imagine the following snippet:
+ *
+ * <pre>
+ * {@code
+ *     int x = 1; // from 3/59 to 4/16
+ *     int y = 2; // from 4/16 to 5/16
+ *     int z = 3; // from 5/16 to 6/16
+ * }
+ * </pre>
+ * </p>
+ * <p>
+ * To execute only the last two statements a user would select intuitively the source
  * range 5/0 to 6/16 (the text without leading white space) which matches exactly the used selection
  * definition.
  * </p>
  * <p>
  * The generated {@link Sequent} has the following form:
  *
  * <pre>
- * <code>
+ * {@code
  * ==>
- * &lt;generalAssumptions&gt; &
- * &lt;preconditions&gt;
+ * <generalAssumptions> &
+ * <preconditions>
  * ->
- * &lt;updatesToStoreInitialValues&gt;
- * &lt;modalityStart&gt;
- * exc=null;try {&lt;methodFrame&gt;&lt;selectedStatements&gt;}catch(java.lang.Exception e) {exc = e}
- * &lt;modalityEnd&gt;
- * (exc = null & &lt;postconditions &gt; & &lt;optionalUninterpretedPredicate&gt;)
- * </code>
+ * <updatesToStoreInitialValues>
+ * <modalityStart>
+ * exc=null;
+ * try {
+ *   <methodFrame><selectedStatements>
+ * } catch(java.lang.Exception e) {
+ *  exc = e
+ * }
+ * <modalityEnd>
+ * (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
+ * }
  * </pre>
  * </p>
  *
  * @author Martin Hentschel
  */
+//spotless:on
 public class ProgramMethodSubsetPO extends ProgramMethodPO {
     /**
      * Contains all undeclared variables used in the method part to execute.

key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java

@@ -16,9 +16,12 @@
 import org.key_project.util.ExtList;
 
 /**
- * In the DL-formulae description of Taclets the program part can have the following form < pi
- * alpha;...; omega > Phi where pi is a prefix consisting of open brackets, try's and so on and
- * omega is the rest of the program. Between the prefix pi and the postfix omega there can stand an
+ * In the DL-formulae description of Taclets the program part can have the following form
+ * {@code < pi
+ * alpha;...; omega > Phi} where {@code pi} is a prefix consisting of open brackets, {@code try}'s
+ * and so on and
+ * omega is the rest of the program. Between the prefix {@code pi} and the postfix {@code omega}
+ * there can stand an
  * arbitrary program. This pattern is realized using this class.
  */
 

key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java

@@ -252,18 +252,21 @@ private StatementBlock getCreateArrayBody(
     }
 
     /**
-     * creates the body of method <code>&lt;createArrayHelper(int
-     * paramLength)&gt;</code> therefore it first adds the statements responsible to take the
+     * creates the body of method {@code <createArrayHelper(int
+     * paramLength)>} therefore it first adds the statements responsible to take the
      * correct one out of the list, then the arrays length attribute is set followed by a call to
-     * <code>&lt;prepare&gt;()</code> setting the arrays fields on their default value.
+     * {@code <prepare>()} setting the arrays fields on their default value.
      *
-     * @param length the final public ProgramVariable <code>length</length> of the array
-     * &#64;param fields the IList<Fields> of the current array
-     * &#64;param createTransient a boolean indicating if a transient array has
-     * to be created (this is special to JavaCard)
-     * &#64;param transientType a ProgramVariable identifying the kind of transient
-     * &#64;return the StatementBlock which is the method's body <br></br>
-     *     <code>
+     * @param length the final public ProgramVariable {@code length} of the array
+     * @param fields the ImmutableList with fields of the current array
+     * @param createTransient a boolean indicating if a transient array has
+     *        to be created (this is special to JavaCard)
+     * @param transientType a ProgramVariable identifying the kind of transient
+     * @return the StatementBlock which is the method's body <br>
+     *         </br>
+     *
+     *         <pre>
+     *  {@code
      *  {
      *    this.<nextToCreate> = this.<nextToCreate>.;
      *    this.<initialized> = false;
@@ -273,7 +276,8 @@ private StatementBlock getCreateArrayBody(
      *    this.<initialized> = true;
      *    return this;
      *   }
-     *   </code>
+     *   }
+     *         </pre>
      */
     private StatementBlock getCreateArrayHelperBody(
             ProgramVariable length,

key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java

@@ -1472,7 +1472,7 @@ public IObserverFunction getStaticInv(KeYJavaType target) {
     }
 
     /**
-     * Returns the special symbol <code>&lt$inv_free&gt;</code> which stands for the static
+     * Returns the special symbol {@code <$inv_free&>}, which stands for the static
      * invariant of a type.
      */
     public IObserverFunction getStaticInvFree(KeYJavaType target) {

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java

@@ -195,7 +195,7 @@ private CrossReferenceServiceConfiguration getServiceConfiguration() {
     }
 
     /**
-     * retrieve the recoder<->key mapping from the associated Recoder2KeY.
+     * retrieve the recoder {@code <->} key mapping from the associated Recoder2KeY.
      *
      * @return the mapping, not null.
      */
@@ -584,7 +584,7 @@ private Constructor<?> getKeYClassConstructor(
     }
 
     /**
-     * store an element to the recoder<->key mapping.
+     * store an element to the recoder {@code <->} key mapping.
      *
      * @param r the recoder element (not null)
      * @param k the key element (not null)

key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java

@@ -11,7 +11,8 @@
 import org.key_project.util.collection.ImmutableArray;
 
 /**
- * Formal parameters require a VariableSpecificationList of size() <= 1 (size() == 0 for abstract
+ * Formal parameters require a VariableSpecificationList of {@code size() <= 1} ({@code size() == 0}
+ * for abstract
  * methods) without initializer (for Java).
  */
 public class ParameterDeclaration extends VariableDeclaration {

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ccatch.java

@@ -200,7 +200,7 @@ public int getChildPositionCode(ProgramElement child) {
      * the replaced child is left untouched.
      *
      * @param p the old child.
-     * @param p the new child.
+     * @param q the new child.
      * @return true if a replacement has occured, false otherwise.
      * @exception ClassCastException if the new child cannot take over the role of the old one.
      */

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakLabelParameterDeclaration.java

@@ -78,7 +78,7 @@ public int getChildPositionCode(ProgramElement child) {
      * the replaced child is left untouched.
      *
      * @param p the old child.
-     * @param p the new child.
+     * @param q the new child.
      * @return true if a replacement has occured, false otherwise.
      * @exception ClassCastException if the new child cannot take over the role of the old one.
      */

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueLabelParameterDeclaration.java

@@ -78,7 +78,7 @@ public int getChildPositionCode(ProgramElement child) {
      * the replaced child is left untouched.
      *
      * @param p the old child.
-     * @param p the new child.
+     * @param q the new child.
      * @return true if a replacement has occured, false otherwise.
      * @exception ClassCastException if the new child cannot take over the role of the old one.
      */

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnValParameterDeclaration.java

@@ -115,7 +115,7 @@ public int getChildPositionCode(ProgramElement child) {
      * the replaced child is left untouched.
      *
      * @param p the old child.
-     * @param p the new child.
+     * @param q the new child.
      * @return true if a replacement has occured, false otherwise.
      * @exception ClassCastException if the new child cannot take over the role of the old one.
      */

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java

@@ -22,8 +22,8 @@
 
 /**
  * Transforms the constructors of the given class to their normalform. The constructor normalform
- * can then be accessed via a methodcall <code>&lt;init&gt;<cons_args)</code>. The visibility of the
- * normalform is the same as for the original constructor.
+ * can then be accessed via a methodcall {@code <init>;<cons_args)}. The visibility of the
+ * normal form is the same as for the original constructor.
  */
 public class ConstructorNormalformBuilder extends RecoderModelTransformer {
 

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Exec.java

@@ -207,7 +207,7 @@ public int getChildPositionCode(ProgramElement child) {
      * the replaced child is left untouched.
      *
      * @param p the old child.
-     * @param p the new child.
+     * @param q the new child.
      * @return true if a replacement has occured, false otherwise.
      * @exception ClassCastException if the new child cannot take over the role of the old one.
      */

key.core/src/main/java/de/uka/ilkd/key/logic/Choice.java

@@ -23,7 +23,7 @@ public class Choice implements Named {
     private final @NonNull String category;
 
     /**
-     * Creates a choice object with name <category&gt:<choice>.
+     * Creates a choice object with name {@code <category>:<choice>}.
      */
     public Choice(String choice, String category) {
         this(new Name(category + ":" + choice), category);

key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java

@@ -8,11 +8,11 @@
 
 
 /**
- * This class defines the equality operator "=". It is a binary predicate accepting arbitrary terms
- * (sort "any") as arguments.
+ * This class defines the logic equality operator {@code =}. It is a binary predicate accepting
+ * arbitrary terms (of sort "any") as arguments.
  *
- * It also defines the formula equivalence operator "<->" (which could alternatively be seen as a
- * Junctor).
+ * It also defines the formula equivalence operator {@code <->} (which could alternatively be seen
+ * as a Junctor).
  */
 public final class Equality extends AbstractSortedOperator {
 
@@ -22,8 +22,9 @@ public final class Equality extends AbstractSortedOperator {
     public static final Equality EQUALS = new Equality(new Name("equals"), Sort.ANY);
 
     /**
-     * the usual 'equivalence' operator '<->' (be A, B formulae then 'A <-> B' is true if and only
-     * if A and B have the same truth value
+     * the usual 'equivalence' operator {@code <->} (be {@code A, B} formulae then {@code A <-> B}
+     * is true
+     * if and only if {@code A} and {@code B} have the same truth value
      */
     public static final Equality EQV = new Equality(new Name("equiv"), Sort.FORMULA);
 

key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java

@@ -18,7 +18,8 @@ public final class Modality extends AbstractSortedOperator {
     private static final Map<String, Modality> nameMap = new LinkedHashMap<>(10);
 
     /**
-     * The diamond operator of dynamic logic. A formula <alpha;>Phi can be read as after processing
+     * The diamond operator of dynamic logic. A formula {@code <alpha;>Phi} can be read as after
+     * processing
      * the program alpha there exists a state such that Phi holds.
      */
     public static final Modality DIA = new Modality(new Name("diamond"));