From 39aaa17635c6e67a409daec579999debf487d644 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 30 Oct 2023 09:09:34 +0100 Subject: [PATCH 1/6] Fix all warnings reported by ./gradlew javadoc --- .../SymbolicLayoutExtractor.java | 39 +++++++++--------- .../po/ProgramMethodPO.java | 23 ++++++----- .../po/ProgramMethodSubsetPO.java | 40 ++++++++++++------- .../ilkd/key/java/ContextStatementBlock.java | 9 +++-- .../java/de/uka/ilkd/key/java/JavaInfo.java | 2 +- .../ilkd/key/java/Recoder2KeYConverter.java | 4 +- .../declaration/ParameterDeclaration.java | 3 +- .../uka/ilkd/key/java/recoderext/Ccatch.java | 2 +- .../CcatchBreakLabelParameterDeclaration.java | 2 +- ...atchContinueLabelParameterDeclaration.java | 2 +- .../CcatchReturnValParameterDeclaration.java | 2 +- .../ConstructorNormalformBuilder.java | 4 +- .../de/uka/ilkd/key/java/recoderext/Exec.java | 2 +- .../java/de/uka/ilkd/key/logic/Choice.java | 2 +- .../de/uka/ilkd/key/logic/op/Equality.java | 11 +++-- .../de/uka/ilkd/key/logic/op/Modality.java | 3 +- .../de/uka/ilkd/key/logic/op/Quantifier.java | 11 +++-- .../de/uka/ilkd/key/logic/op/SubstOp.java | 8 ++-- .../de/uka/ilkd/key/logic/op/WarySubstOp.java | 3 +- .../java/de/uka/ilkd/key/pp/LogicPrinter.java | 2 +- .../java/de/uka/ilkd/key/pp/NotationInfo.java | 28 +++++++------ .../java/de/uka/ilkd/key/proof/Counter.java | 2 +- .../key/proof/init/AbstractOperationPO.java | 23 ++++++----- .../init/FunctionalOperationContractPO.java | 18 ++++----- .../key/proof/init/WellDefinednessPO.java | 12 +++--- ...termediatePresentationProofFileParser.java | 2 + .../key/rule/AbstractLoopInvariantRule.java | 2 +- .../de/uka/ilkd/key/rule/AntecTaclet.java | 6 +-- .../java/de/uka/ilkd/key/rule/FindTaclet.java | 10 ++--- .../ilkd/key/rule/LoopScopeInvariantRule.java | 2 + .../de/uka/ilkd/key/rule/NoFindTaclet.java | 9 +++-- .../de/uka/ilkd/key/rule/NoPosTacletApp.java | 10 ++++- .../de/uka/ilkd/key/rule/QueryExpand.java | 10 +++-- .../de/uka/ilkd/key/rule/RewriteTaclet.java | 19 +++++---- .../java/de/uka/ilkd/key/rule/SuccTaclet.java | 17 ++++---- .../key/rule/inst/ProgramSVInstantiation.java | 4 +- .../ilkd/key/rule/inst/SVInstantiations.java | 18 +++++---- .../MatchProgramSVInstruction.java | 2 +- .../ilkd/key/rule/merge/CloseAfterMerge.java | 8 ++-- .../key/rule/metaconstruct/UnwindLoop.java | 16 +++++++- .../WhileLoopTransformation.java | 2 +- .../AbstractAuxiliaryContractImpl.java | 22 +++++----- .../key/speclang/PositionedLabeledString.java | 5 ++- .../key/speclang/WellDefinednessCheck.java | 2 +- .../quantifierHeuristics/HandleArith.java | 5 ++- .../termgenerator/RootsGenerator.java | 6 +-- .../key/util/mergerule/MergeRuleUtils.java | 8 ++-- .../key/gui/prooftree/GUIProofTreeModel.java | 36 +++++++++-------- .../ilkd/key/gui/settings/SettingsPanel.java | 14 ++++--- .../util/collection/DefaultImmutableMap.java | 10 +++-- .../util/collection/ImmutableMap.java | 3 +- .../org/key_project/util/java/XMLUtil.java | 12 +++--- .../util/reflection/ClassLoaderUtil.java | 2 +- .../exploration/ProofExplorationService.java | 18 +++++++-- .../java/recoder/io/ArchiveDataLocation.java | 9 +++-- .../java/recoder/io/DataFileLocation.java | 13 ++++-- .../main/java/recoder/io/DataLocation.java | 8 +++- .../main/java/recoder/io/PropertyNames.java | 18 ++++----- .../recoder/java/PackageSpecification.java | 2 +- .../java/recoder/java/ProgramElement.java | 2 +- .../declaration/ParameterDeclaration.java | 3 +- .../recoder/java/expression/operator/New.java | 20 +++++++--- .../SpecialConstructorReference.java | 2 +- .../recoder/java/statement/LoopStatement.java | 2 +- .../java/recoder/java/statement/Switch.java | 2 +- .../src/main/java/recoder/util/Equality.java | 10 ++--- recoder/src/main/java/recoder/util/Order.java | 26 +++++++----- 67 files changed, 393 insertions(+), 261 deletions(-) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java index f41261db8fe..51a53013ff4 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java @@ -44,19 +44,20 @@ * Example program: * * 
- * 
- * 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
+ *         }
+ *     }
  * }
- * 
  *
* * If the symbolic execution stops at the return statement, two memory layouts are possible. In the @@ -68,15 +69,17 @@ * The following code snippet shows how to use this class: * * 
- * 
- * SymbolicLayoutExtractor e = new SymbolicLayoutExtractor(node);
- * e.analyse();
- * for (int i = 0; i < e.getLayoutsCount(); i++) {
- *    ImmutableList<ISymbolicEquivalenceClass> 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<ISymbolicEquivalenceClass> equivalenceClasses = e.getEquivalenceClasses(i);
+ *         ISymbolicLayout initial = e.getInitialLayout(i);
+ *         ISymbolicLayout current = e.getCurrentLayout(i);
+ *     }
  * }
- * 
+ *
* *

*

diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java index 1056f15b599..53e80b46f2b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java +++ b/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: * * 

- * 
+ * {@code
  * ==>
- * <generalAssumptions> &
- * <preconditions>
+ *  &
+ * 
  * ->
- * <updatesToStoreInitialValues>
- * <modalityStart>
- * exc=null;try {<methodBodyStatement>}catch(java.lang.Exception e) {exc = e}
- * <modalityEnd>
- * (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
- * 
+ * 
+ * 
+ * exc=null;
+ * try {
+ *   
+ * } catch(java.lang.Exception e) {
+ *    exc = e
+ * }
+ * 
+ *  (exc = null &  & )
+ * }
  *
*

* diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java index 838022ca795..ba8232f5f3e 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java @@ -38,11 +38,18 @@ * position of the previous statement is exactly the start position of the following statement. *

*

- * Imagine the following snippet: 

- * 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
- *
To execute only the last two statements a user would select intuitively the source + * Imagine the following snippet: + * + * 
+ * {
+ *     @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
+ * }
+ *
+ * + * 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. *

@@ -50,17 +57,22 @@ * The generated {@link Sequent} has the following form: * * 
- * 
+ * {@code
  * ==>
- * <generalAssumptions> &
- * <preconditions>
+ *  &
+ * 
  * ->
- * <updatesToStoreInitialValues>
- * <modalityStart>
- * exc=null;try {<methodFrame><selectedStatements>}catch(java.lang.Exception e) {exc = e}
- * <modalityEnd>
- * (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
- * 
+ * 
+ * 
+ * exc=null;
+ * try {
+ *   
+ * } catch(java.lang.Exception e) {
+ *  exc = e
+ * }
+ * 
+ * (exc = null &  & )
+ * }
  *
*

* diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java index 1dd0d76426a..408d81bbdb1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java +++ b/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. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java index c0cfecba621..7703c9f34d3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java +++ b/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 <$inv_free> 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) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 8e21443c5ea..cc46b246c27 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/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) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java index 0ef03c77656..75c08a72be7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ccatch.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ccatch.java index 61e55c05026..719a0bdd510 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ccatch.java +++ b/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. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakLabelParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakLabelParameterDeclaration.java index 0d05a0c9076..187680e608a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakLabelParameterDeclaration.java +++ b/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. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueLabelParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueLabelParameterDeclaration.java index b1b75b5c5ac..c808cbaff9a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueLabelParameterDeclaration.java +++ b/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. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnValParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnValParameterDeclaration.java index 13704cad358..702541dbc64 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnValParameterDeclaration.java +++ b/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. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java index f204a773ee4..345a89bb8c9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java +++ b/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 <init>. The visibility of the - * normalform is the same as for the original constructor. + * can then be accessed via a methodcall {@code ;:}. */ public Choice(String choice, String category) { this(new Name(category + ":" + choice), category); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java index cb75edd182a..89b5f6c6b7e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java @@ -8,10 +8,12 @@ /** - * This class defines the equality operator "=". It is a binary predicate accepting arbitrary terms + * This class defines the equality operator {@code ==}. It is a binary predicate accepting arbitrary + * terms * (sort "any") as arguments. * - * It also defines the formula equivalence operator "<->" (which could alternatively be seen as a + * It also defines the formula equivalence operator {@code <->} (which could alternatively be seen + * as a * Junctor). */ public final class Equality extends AbstractSortedOperator { @@ -22,8 +24,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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java index f27939106a9..be24ee83a7b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java +++ b/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 nameMap = new LinkedHashMap<>(10); /** - * The diamond operator of dynamic logic. A formula Phi can be read as after processing + * The diamond operator of dynamic logic. A formula {@code 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")); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java index 7dc70bca526..5d19f12697c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java @@ -15,14 +15,17 @@ public final class Quantifier extends AbstractSortedOperator { public static final Name EX_NAME = new Name("exists"); /** - * the usual 'forall' operator 'all' (be A a formula then 'all x.A' is true if and only if for - * all elements d of the universe A{x<-d} (x substituted with d) is true + * the usual {@code forall} operator 'all' (be A a formula then {@code forall x.A} is true if + * and only if for + * all elements d of the universe {@code A{x<-d}} (x substituted with d) is true */ public static final Quantifier ALL = new Quantifier(ALL_NAME); /** - * the usual 'exists' operator 'ex' (be A a formula then 'ex x.A' is true if and only if there - * is at least one elements d of the universe such that A{x<-d} (x substituted with d) is true + * the usual {@code exists}-operator (be {@code A} a formula then {@code exists x; A} is true if + * and only if there + * is at least one element d of the universe such that {@code A{x<-d}} (x substituted with d) is + * true */ public static final Quantifier EX = new Quantifier(EX_NAME); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java index 8dc187f808f..c4107835584 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java @@ -39,9 +39,11 @@ public Sort sort(ImmutableArray terms) { /** - * @return true iff the sort of the subterm 0 of the given term has the same sort as or a - * subsort of the variable to be substituted and the term's arity is 2 and the numer of - * variables bound there is 0 for the 0th subterm and 1 for the 1st subterm. + * checks whether the sort of the subterm 0 of the given term has the same sort as or a + * subsort of the variable to be substituted and the term's arity is 2 and the number of + * variables bound there is 0 for the 0th subterm and 1 for the 1st subterm. + * + * @throws TermCreationException if the check fails */ @Override protected void additionalValidTopLevel(Term term) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/WarySubstOp.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/WarySubstOp.java index 5ddb7b56c30..697c482eed4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/WarySubstOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/WarySubstOp.java @@ -12,7 +12,8 @@ public final class WarySubstOp extends SubstOp { /** - * the wary substitution operator {var<-term}'. {x<-d}'A(x) means replace all free occurrences + * the wary substitution operator {@code {var<-term}'}. {@code {x<-d}'A(x)} means replace all + * free occurrences * of variable x in A with d, however without replacing x with a non-rigid A below modalities */ public static final SubstOp SUBST = new WarySubstOp(new Name("subst")); diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index e42e7ee8cdd..9ae40374f80 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -1345,7 +1345,7 @@ public void printPostfixTerm(Term t, int ass, String name) { * the format is like * * 
-     * p & q
+     * {@code p & q}
      *
*

* The subterms are printed using {@link #printTermContinuingBlock(Term)}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java index 7dae46511af..fd9313c37fb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java @@ -29,50 +29,52 @@ * The Notation associated with an operator might change. New Notations can be added. * *

- * The next lines describe a general rule how to determine priorities and associativities: + * The next lines describe a general rule how to determine priorities and associativity: * * One thing we need to know from the pretty printer: Given a term t containg s as * proper subterm. Then s is printed in parentheses when the priority of the top level * symbol of s is strict less than the associativity of the position where s * occurs. For example: *

- * Let the priority of AND be 30 and the associativities for each of its subterms - * be 40; ORs priority is 20 and the associativites are both 30 then + * Let the priority of AND be 30 and the associativity for each of its subterms + * be 40; ORs priority is 20 and the associativity are both 30 then *

    - *
  • formula (p & q) | r is pretty printed as p & q | r as the priority of & is + *
  • formula {@code (p & q) | r} is pretty printed as {@code p & q | r} as the priority of + * {@code &} is * 30 which is (greater or) equal than the associativity of ORs left subterm which is * 30.
    • - *
  • In contrast the formula p & (q | r) is pretty printed as p & (q | r) as the + *
  • In contrast the formula {@code p & (q | r)} is pretty printed as {@code p & (q | r)} as the * priority of OR is 20 which is less than the associativity of ANDs left subterm, * which is 40.
    • *
* * A general rule to determine the correct priority and associativity is to use: - * + *

* Grammar rules whose derivation delivers a syntactical correct logic term should follow a standard * numbering scheme, which is used as indicator for priorities and associativites, e.g. by simply - * reading the grammar rule

term60 ::= term70 (IMP term70)?
we get + * reading the grammar rule
{@code term60 ::= term70 (IMP term70)?}
we get * the priority of IMP, which is 60. The associativities of IMPs subterms * are not much more difficult to determine, namely the left subterm has associativity 70 * and in this case its the same for the right subterm (70). + *

*

* There are exceptional cases for *

    *
  • infix function symbols that are left associative e.g. -, +
    - * term90 ::= term100 (PLUS term100)*
    then the associative for the right + * {@code term90 ::= term100 (PLUS term100)* } then the associative for the right * subterm is increased by 1, i.e. here we have a priority of 90 for PLUS * as infix operator, a left associativity of 100 and a right associativity of * 101
    • - *
  • update and substituition terms: for them their associativity is determined dynamically by the + *
  • update and substitution terms: for them their associativity is determined dynamically by the * pretty printer depending if it is applied on a formula or term. In principal there should be two * different rules in the parser as then we could reuse the general rule from above, but there are * technical reasons which causes this exception.
    • *
  • some very few rules do not follow the usual parser design e.g. like - *
    R_PRIO ::= SubRule_ASS1 | SubRule_ASS2
    where - *
    SubRule_ASS2 ::= OP SubRule_ASS1
    Most of these few rules could + *
    {@code R_PRIO ::= SubRule_ASS1 | SubRule_ASS2 }
    where + *
    {@code SubRule_ASS2 ::= OP SubRule_ASS1}
    Most of these few rules could * in general be rewritten to fit the usual scheme e.g. as - *
    R_PRIO ::= (OP)? SubRule_ASS1
    using the priorities and - * associativities of the so rewritten rules (instead of rewriting them actually) is a way to cope + *
    {@code R_PRIO ::= (OP)? SubRule_ASS1}
    using the priorities and + * associativity of the so rewritten rules (instead of rewriting them actually) is a way to cope * with them.
    • *
*/ diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Counter.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Counter.java index 8d9bd600257..b52df2e0996 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Counter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Counter.java @@ -4,7 +4,7 @@ package de.uka.ilkd.key.proof; -/** Proof-specific counter object: taclet names, var names, node numbers, &c */ +/** Proof-specific counter object: taclet names, var names, node numbers, etc */ public class Counter { private final String name; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java index f13232bdf7e..2d9beca1832 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java @@ -43,17 +43,22 @@ * The generated {@link Sequent} has the following form: * * 
- * 
+ * {@code
  * ==>
- * <generalAssumptions> &
- * <preconditions>
+ *  &
+ * 
  * ->
- * <updatesToStoreInitialValues>
- * <modalityStart>
- * exc=null;try {<customCode>}catch(java.lang.Throwable e) {exc = e}
- * <modalityEnd>
- * (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
- * 
+ * 
+ * 
+ * exc=null;
+ * try {
+ *   
+ * } catch (java.lang.Throwable e) {
+ *    exc = e
+ * }
+ * 
+ * (exc = null &  & )
+ * }
  *
*

*

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java index eac95d0d8ae..b00fe7b6233 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java @@ -45,17 +45,17 @@ * The generated {@link Sequent} has the following form: * * 

- * 
+ * {@code
  * ==>
- * <generalAssumptions> &
- * <preconditions>
+ *  &
+ * 
  * ->
- * <updatesToStoreInitialValues>
- * <modalityStart>
- * exc=null;try {<methodBodyExpand>}catch(java.lang.Throwable e) {exc = e}
- * <modalityEnd>
- * (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
- * 
+ * 
+ * 
+ * exc=null;try {}catch(java.lang.Throwable e) {exc = e}
+ * 
+ * (exc = null &  & )
+ * }
  *
*

*/ diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java index 4bf418301d7..474bca4516d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java @@ -34,13 +34,13 @@ * The generated {@link Sequent} has the following form: * * 
- * 
+ * {@code
  * ==>
- * WD(<generalAssumptions> && <preconditions>) &
- * (<generalAssumptions> & <preconditions>
- *    -> WD(<otherClauses>) &
- *       {anon^assignable}WD(<postconditions>)
- * 
+ * WD( && ) &
+ * ( & 
+ *    -> WD() &
+ *       {anon^assignable}WD()
+ * }
  *
*

* diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index 9e9645a271d..4e5b2ad248c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -35,6 +35,7 @@ *

* * 

+ * {@code
  * BranchNodeIntermediate "dummy ID"
  * - AppNodeIntermediate
  * - AppNodeIntermediate
@@ -46,6 +47,7 @@
  *   + BranchNodeIntermediate "x <= 0"
  *     > AppNodeIntermediate
  *     > ...
+ * }
  *
*

*

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java index 4397016b196..9fe56d2aa02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java @@ -338,7 +338,7 @@ protected static boolean isModalityTerm(final Term progPost) { * @param tb The {@link TermBuilder} object. * @param t1 The first formula of the conjunction; may be null. * @param t2 The second formula of the conjunction; may not be null. - * @return Returns t2 if t1 is null and t1 & t2 if both aren't null. + * @return returns {@code t2} if {@code t1} is null and {@code t1 & t2} if both aren't null. */ protected static Term and(TermBuilder tb, Term t1, Term t2) { assert t2 != null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AntecTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AntecTaclet.java index c4f4e3b4622..758507db4f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AntecTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AntecTaclet.java @@ -29,11 +29,11 @@ public class AntecTaclet extends FindTaclet { * @param applPart contains the application part of an Taclet that is the if-sequent, the * variable conditions * @param goalTemplates a list of goal descriptions. - * @param heuristics a list of heurisics for the Taclet - * @param attrs attributes for the Taclet; these are boolean values indicating a noninteractive + * @param heuristics a list of heuristics for the Taclet + * @param attrs attributes for the Taclet; these are boolean values indicating a non-interactive * or recursive use of the Taclet. * @param find the find term of the Taclet - * @param prefixMap a ImmMap that contains the prefix for each + * @param prefixMap a ImmutableMap that contains the prefix for each * SchemaVariable in the Taclet */ public AntecTaclet(Name name, TacletApplPart applPart, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/FindTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/FindTaclet.java index b9980078f27..4f191bfb65a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/FindTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/FindTaclet.java @@ -45,12 +45,12 @@ public abstract class FindTaclet extends Taclet { * conditions * @param goalTemplates a IList that contains all goaltemplates of the * taclet (these are the instructions used to create new goals when applying the Taclet) - * @param ruleSets a IList that contains all rule sets the Taclet is attached to + * @param ruleSets a ImmutableList that contains all rule sets the Taclet is attached to * @param attrs the TacletAttributes encoding if the Taclet is non-interactive, recursive or * something like that * @param find the Term that is the pattern that has to be found in a sequent and the places * where it matches the Taclet can be applied - * @param prefixMap a ImmMap that contains the prefix for each + * @param prefixMap a ImmutableMap that contains the prefix for each * SchemaVariable in the Taclet */ protected FindTaclet(Name name, TacletApplPart applPart, @@ -69,14 +69,14 @@ protected FindTaclet(Name name, TacletApplPart applPart, * @param name the Name of the taclet * @param applPart the TacletApplPart that contains the if-sequent, the not-free and new-vars * conditions - * @param goalTemplates a IList that contains all goaltemplates of the + * @param goalTemplates an ImmutableList that contains all goaltemplates of the * taclet (these are the instructions used to create new goals when applying the Taclet) - * @param ruleSets a IList that contains all rule sets the Taclet is attached to + * @param ruleSets an ImmutableList that contains all rule sets the Taclet is attached to * @param attrs the TacletAttributes encoding if the Taclet is non-interactive, recursive or * something like that * @param find the Term that is the pattern that has to be found in a sequent and the places * where it matches the Taclet can be applied - * @param prefixMap a ImmMap that contains the prefix for each + * @param prefixMap an ImmutableMap that contains the prefix for each * SchemaVariable in the Taclet */ protected FindTaclet(Name name, TacletApplPart applPart, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java index a2455874154..52fa14c216a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java @@ -63,6 +63,7 @@ *

* * 
+ * {@code
  * \Gamma ==> {U}Inv, \Delta
  * \Gamma, {U'}Inv ==> \Delta, {U'}[\pi
  *    boolean x = true;
@@ -72,6 +73,7 @@
  *    ((x = TRUE -> \phi) & (x = FALSE -> Inv))
  * ---------------------------------------------------------- loopInvariant
  * \Gamma ==> {U}[\pi l: while (nse) { p } \omega]\phi, Delta
+ * }
  *
* * @author Dominic Scheurer diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NoFindTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NoFindTaclet.java index 8e5296382c7..b16e1f7c7ad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/NoFindTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/NoFindTaclet.java @@ -22,16 +22,17 @@ public class NoFindTaclet extends Taclet { /** - * creates a Schematic Theory Specific Rule (Taclet) with the given parameters. + * creates a {@link Taclet} (previously Schematic Theory Specific Rule) with the given + * parameters. * * @param name the name of the Taclet - * @param applPart contains the application part of an Taclet that is the if-sequent, the + * @param applPart contains the application part of a Taclet that is the if-sequent, the * variable conditions - * @param goalTemplates the IList containg all goal descriptions of the + * @param goalTemplates the IList containing all goal descriptions of the * taclet to be created * @param ruleSets a list of rule sets for the Taclet * @param attrs attributes for the Taclet; these are boolean values - * @param prefixMap a ImmMap that contains the prefix for each + * @param prefixMap a ImmutableMap that contains the prefix for each * SchemaVariable in the Taclet * @param choices the SetOf to which this taclet belongs to */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java index 61918fb6f5a..746fdc4eeb6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java @@ -292,8 +292,14 @@ public PosInOccurrence posInOccurrence() { } /** - * PRECONDITION: ifFormulaInstantiations () == null && ( pos == null || - * termConstraint.isSatisfiable () ) + * PRECONDITION: + * + * 
+     *  {@code
+     * ifFormulaInstantiations () == null &&
+     *   ( pos == null || termConstraint.isSatisfiable () )
+     * }
+     *
* * @return TacletApp with the resulting instantiations or null */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java index 84759d882b1..ab1aff53743 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java @@ -99,11 +99,13 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) * @param services * @param query The query on which the query expand rule is applied * @param instVars If null, then the result of the query can be stored in a constant (e.g. - * res=query(a)). Otherwise it is a list of logical variables that can be instantiated + * {@code res=query(a)}). Otherwise, it is a list of logical variables that can be + * instantiated * (using the rules allLeft, exRight) and therefore the result of the query must be - * stored by function that depends on instVars (e.g. forall i; res(i)=query(i)). The list - * may be empty even if it not null. - * @return The formula (!{U}result=res_query) & query()=res_query + * stored by function that depends on instVars (e.g. {@code \forall i; res(i)=query(i)}). + * The list + * may be empty even if it is not null. + * @return The formula {@code (!{U}result=res_query) & query()=res_query} * @author Richard Bubel * @author gladisch */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java index d3c84aa5691..e8cbd36346c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java @@ -46,18 +46,23 @@ public class RewriteTaclet extends FindTaclet { /** * If the surrounding formula has been decomposed completely, the find-term will NOT appear on - * the SUCcedent. The formula "wellformed(h)" in "wellformed(h) ==>" or in "==> wellformed(h) -> - * (inv(h) = inv(h2))" or in "==> \if(b) \then(!wellformed(h)) \else(!wellformed(h2))" has - * antecedent polarity. The formula "wellformed(h)" in "wellformed(h) <-> wellformed(h2) ==>" + * the SUCcedent. The formula {@code wellformed(h)} in {@code wellformed(h) ==>} or in + * {@code ==> wellformed(h) -> + * (inv(h) = inv(h2))} or in {@code ==> \if(b) \then(!wellformed(h)) \else(!wellformed(h2))} has + * antecedent polarity. The formula {@code wellformed(h)} in + * {@code wellformed(h) <-> wellformed(h2) ==>} * has NO antecedent polarity. */ public static final int ANTECEDENT_POLARITY = 4; /** * If the surrounding formula has been decomposed completely, the find-term will NOT appear on - * the ANTEcedent. The formula "wellformed(h)" in "==> wellformed(h)" or in "wellformed(h) -> - * (inv(h) = inv(h2)) ==>" or in "\if(b) \then(!wellformed(h)) \else(!wellformed(h2)) ==>" has - * succedent polarity. The formula "wellformed(h)" in "wellformed(h) <-> wellformed(h2) ==>" has + * the ANTEcedent. The formula {@code wellformed(h)} in {@code==> wellformed(h)} or in + * {@code wellformed(h) -> + * (inv(h) = inv(h2)) ==>} or in {@code \if(b) \then(!wellformed(h)) \else(!wellformed(h2)) ==>} + * has + * succedent polarity. The formula {@code wellformed(h)} in + * {@code wellformed(h) <-> wellformed(h2) ==>} has * NO succedent polarity. */ public static final int SUCCEDENT_POLARITY = 8; @@ -89,7 +94,7 @@ public class RewriteTaclet extends FindTaclet { * @param attrs the TacletAttributes; these are boolean values indicating a noninteractive or * recursive use of the Taclet. * @param find the find term of the Taclet - * @param prefixMap a ImmMap that contains the prefix for each + * @param prefixMap an ImmutableMap that contains the prefix for each * SchemaVariable in the Taclet * @param p_applicationRestriction an int defining state restrictions of the taclet (required * for location check) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SuccTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SuccTaclet.java index 1a3e5705d11..5d3f3b0ce25 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/SuccTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SuccTaclet.java @@ -23,19 +23,20 @@ public class SuccTaclet extends FindTaclet { private final boolean ignoreTopLevelUpdates; /** - * creates a Schematic Theory Specific Rule (Taclet) with the given parameters that works on the - * succedent. + * creates a {@link Taclet} (old name Schematic Theory Specific Rule) with the given parameters + * that works on the succedent. * - * @param name the name of the Taclet - * @param applPart contains the application part of an Taclet that is the if-sequent, the + * @param name the name of the {@link Taclet} + * @param applPart contains the application part of a taclet that is the if-sequent, the * variable conditions * @param goalTemplates a list of goal descriptions. - * @param heuristics a list of heurisics for the Taclet - * @param attrs attributes for the Taclet; these are boolean values indicating a noninteractive + * @param heuristics a list of heuristics for the Taclet + * @param attrs attributes for the Taclet; these are boolean values indicating a non-interactive * or recursive use of the Taclet. * @param find the find term of the Taclet - * @param prefixMap a ImmMap that contains the prefix for each - * SchemaVariable in the Taclet + * @param prefixMap an ImmutableMap from {@link SchemaVariable} to {@link TacletPrefix} that + * contains + * the prefix for each SchemaVariable in the taclet */ public SuccTaclet(Name name, TacletApplPart applPart, ImmutableList goalTemplates, ImmutableList heuristics, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java index a5b639ba773..383739c4bdc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java @@ -13,7 +13,7 @@ /** - * this class wrapps a ImmMap and is used to store instantiations + * this class wrapps an {@link ImmutableList} and is used to store instantiations * of schemavariables. The class is immutable, this means changing its content will result in * creating a new object. */ @@ -111,7 +111,7 @@ public JavaProgramElement getInstantiation(SchemaVariable sv) { /** * returns iterator of the listped pair (SchemaVariables, JavaProgramElement) * - * @return the Iterator> + * @return the Iterator */ public Iterator iterator() { return list.iterator(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index fb3da8cf978..8494913ea35 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -30,9 +30,10 @@ import org.key_project.util.collection.ImmutableSLList; /** - * This class wraps a ImmMap> and is used to store - * instantiations of schemavariables. The class is immutable, this means changing its content will - * result in creating a new object. + * This class wraps an {@link ImmutableMap} from {@link SchemaVariable} to + * {@link InstantiationEntry} + * and is used to store instantiations of schemavariables. The class is immutable, + * this means changing its content results in creating a new object. */ public class SVInstantiations implements EqualsModProofIrrelevancy { /** the empty instantiation */ @@ -251,7 +252,7 @@ private SVInstantiations rebuildSorts(Services services) { * already, the new pair is taken without a warning. * * @param sv the SchemaVariable to be instantiated - * @param entry the InstantiationEntry + * @param entry the InstantiationEntry * @return SVInstantiations the new SVInstantiations containing the given pair */ public SVInstantiations add(SchemaVariable sv, InstantiationEntry entry, Services services) { @@ -288,7 +289,7 @@ public SVInstantiations addInteresting(SchemaVariable sv, Name name, Services se * instantiated already, the new pair is taken without a warning. * * @param sv the SchemaVariable to be instantiated - * @param entry the InstantiationEntry the SchemaVariable is instantiated with + * @param entry the InstantiationEntry the SchemaVariable is instantiated with */ public SVInstantiations replace(SchemaVariable sv, InstantiationEntry entry, Services services) { @@ -379,7 +380,8 @@ public boolean isInstantiated(SchemaVariable sv) { /** * returns the instantiation of the given SchemaVariable * - * @return the InstantiationEntry the SchemaVariable will be instantiated with, null if no + * @return the InstantiationEntry the SchemaVariable will be instantiated with, {@code null} if + * no * instantiation is stored */ public InstantiationEntry getInstantiationEntry(SchemaVariable sv) { @@ -484,9 +486,9 @@ public Iterator svIterator() { } /** - * returns iterator of the mapped pair (SchemaVariables, InstantiationEntry) + * returns iterator of the mapped pair {@code (SchemaVariables, InstantiationEntry)} * - * @return the Iterator> + * @return the Iterator */ public Iterator>> pairIterator() { return map.iterator(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java index 07af5f0a484..e37da149324 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java @@ -30,7 +30,7 @@ public MatchProgramSVInstruction(ProgramSV sv) { /** * tries to add the pair (this,pe) to the match conditions. If possible the resulting * match conditions are returned, otherwise null. Such an addition can fail, e.g. if - * already a pair (this,x) exists where x<>pe + * already a pair (this,x) exists where x!=pe */ protected MatchConditions addInstantiation(ProgramElement pe, MatchConditions matchCond, Services services) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java index b162b10236f..b03fb381602 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java @@ -240,7 +240,8 @@ private Term getSyntacticWeakeningFormula(CloseAfterMergeRuleBuiltInRuleApp clos * @param constsToReplace Skolem constants to replace before the universal closure. * @param services The services object. * @return A new term which is equivalent to the universal closure of the argument term, with - * Skolem constants in constsToReplace having been replaced by fresh variables before. + * Skolem constants in {@code constsToReplace} having been replaced by fresh variables + * before. */ private Term allClosure(final Term term, final HashSet constsToReplace, Services services) { @@ -278,8 +279,9 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { * @param mergeNodeState The SE state for the merge node; needed for adding an implicative * premise ensuring the soundness of merge rules. * @param partnerState The SE state for the partner node. - * @param pc The program counter common to the two states -- a formula of the form U\<{...}\> - * PHI, where U is an update in normal form and PHI is a DL formula). + * @param pc The program counter common to the two states -- a formula of the form + * {@code U\<{...}\> + * PHI}, where U is an update in normal form and PHI is a DL formula). * @param newNames The set of new names (of Skolem constants) introduced in the merge. * @return A complete {@link CloseAfterMergeRuleBuiltInRuleApp}. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java index 2aa38f06604..e906accd693 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java @@ -15,11 +15,23 @@ /** * This class is used to perform program transformations needed for the symbolic execution of a - * loop. It unwinds the loop: e.g. + * loop. It unwinds the loop: e.g. + * + * 
+ * {@code
  * while ( i<10 ) {
  *   i++
  * }
- *  becomes if (i<10) l1:{ l2:{ i++; } while (i<10) { i++; } }
+ * }
+ *
+ * + * becomes + * + * 
+ * {@code
+ * if (i<10) l1:{ l2:{ i++; } while (i<10) { i++; } }
+ * }
+ *
* */ public class UnwindLoop extends ProgramTransformer { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java index 92c05d6ee0c..14bc6a66ec1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java @@ -377,7 +377,7 @@ public void performActionOnContinue(Continue x) { } } - /** + /* * * public void performActionOnFor(For x) { ExtList changeList = stack.peek(); if * (replaceBreakWithNoLabel==0) { //most outer for loop if (changeList.getFirst() == CHANGED) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java index 58df55115ce..1cb413878ca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java @@ -145,7 +145,7 @@ public abstract class AbstractAuxiliaryContractImpl implements AuxiliaryContract * @param freeModifiesClauses this contract's free modifies clauses on every heap. * @param infFlowSpecs this contract's information flow specifications. * @param variables this contract's variables. - * @param transactionApplicable whether or not this contract is applicable for transactions. + * @param transactionApplicable whether this contract is applicable for transactions. * @param hasMod a map specifying on which heaps this contract has a modified clause. * @param functionalContracts the functional contracts corresponding to this contract. */ @@ -173,7 +173,7 @@ public AbstractAuxiliaryContractImpl(final String baseName, final StatementBlock assert variables.breakFlags != null; assert variables.continueFlags != null; assert variables.exception != null; - assert variables.remembranceHeaps != null && variables.remembranceHeaps.size() > 0; + assert variables.remembranceHeaps != null && !variables.remembranceHeaps.isEmpty(); assert variables.remembranceLocalVariables != null; this.baseName = baseName; this.block = block; @@ -790,7 +790,7 @@ protected Map createReplacementMap(final Term newHeap, final Terms n * @param baseHeap base heap. * @param heapLDT heap LDT. * @param services services. - * @return a HTML representation of this contract's modifies clauses. + * @return an HTML representation of this contract's modifies clauses. */ private String getHtmlMods(final LocationVariable baseHeap, final HeapLDT heapLDT, final Services services) { @@ -815,7 +815,7 @@ private String getHtmlMods(final LocationVariable baseHeap, final HeapLDT heapLD * @param baseHeap base heap. * @param heapLDT heap LDT. * @param services services. - * @return a HTML representation of this contract's preconditions. + * @return an HTML representation of this contract's preconditions. */ private String getHtmlPres(final LocationVariable baseHeap, final HeapLDT heapLDT, final Services services) { @@ -835,7 +835,7 @@ private String getHtmlPres(final LocationVariable baseHeap, final HeapLDT heapLD * @param baseHeap base heap. * @param heapLDT heap LDT. * @param services services. - * @return a HTML representation of this contract's postconditions. + * @return an HTML representation of this contract's postconditions. */ private String getHtmlPosts(final LocationVariable baseHeap, final HeapLDT heapLDT, final Services services) { @@ -1063,7 +1063,7 @@ protected static abstract class Creator extends Ter * @param returns the contract's postcondition for abrupt termination with {@code return} * statements. * @param signals the contract's postcondition for abrupt termination due to abrupt - * termintation. + * termination. * @param signalsOnly a term specifying which uncaught exceptions may occur. * @param diverges a diverges clause. * @param assignables map from every heap to an assignable term. @@ -1298,7 +1298,7 @@ private Term conditionPostconditions(final Map flags, /** * * @param flag an abrupt termination flag. - * @param postcondition a postcondition for abrupt termination with the specifed flag. + * @param postcondition a postcondition for abrupt termination with the specified flag. * @return a part of the postcondition. */ private Term conditionPostcondition(final ProgramVariable flag, final Term postcondition) { @@ -1445,7 +1445,7 @@ private Map buildFreeModifiesClauses() { * @param postconditions the contracts' postconditions. * @param modifiesClauses the contracts' modifies clauses. * @param infFlowSpecs the contracts' information flow specifications. - * @return a set of one or two contracts (depending on whether the {@code diverges} clause + * @return a set of one or two contracts depending on whether the {@code diverges} clause * is trivial (i.e., {@code true} or {@code false}) or not. */ private ImmutableSet create(final Map preconditions, @@ -1487,7 +1487,7 @@ private ImmutableSet create(final Map preconditions, * @param freeModifiesClauses this contract's free modifies clauses on every heap. * @param infFlowSpecs this contract's information flow specifications. * @param variables this contract's variables. - * @param transactionApplicable whether or not this contract is applicable for transactions. + * @param transactionApplicable whether this contract is applicable for transactions. * @param hasMod a map specifying on which heaps this contract has a modifies clause. * @param hasFreeMod a map specifying on which heaps this contract has a free modifies * clause. @@ -1532,7 +1532,7 @@ private Map addNegatedDivergesConditionToPreconditions( } /** - * This class is used to to combine multiple contracts for the same block and apply them + * This class is used to combine multiple contracts for the same block and apply them * simultaneously. It should be overridden in every subclass. * * @param the type of the subclass. @@ -1603,7 +1603,7 @@ public Combinator(final T[] contracts, final Services services) { /** * * @param contracts the contract's to sort. - * @return an array containg the specified contracts sorted alphabetically by name. + * @return an array containing the specified contracts sorted alphabetically by name. */ private T[] sort(final T[] contracts) { // sort contracts alphabetically (for determinism) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedLabeledString.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedLabeledString.java index ea379a65471..3d4897492ff 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedLabeledString.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedLabeledString.java @@ -10,8 +10,9 @@ /** * A positionedString with labels, which can then be passed over to the translated term. For the - * moment, this is used to distinguish implicit specifications from explicit ones and '&' from '&&' - * (logical and shortcut 'and') as well as '|' from '||' (logical and shortcut 'or'). + * moment, this is used to distinguish implicit specifications from explicit ones and {@code &} from + * {@code &&} + * (logical and shortcut 'and') as well as {@code |} from {@code ||} (logical and shortcut 'or'). * * @author Michael Kirsten */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java index bbe5757d508..8a5f53edea1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java @@ -916,7 +916,7 @@ public static boolean isOn() { /** * collects terms for precondition, assignable clause and other specification elements, and - * postcondition & signals-clause + * {code postcondition {@code &} signals-clause} */ public final POTerms createPOTerms() { final Condition pre = this.getRequires(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java index 4c535d7c968..630b820714d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java @@ -18,8 +18,9 @@ import org.key_project.util.LRUCache; /** - * This class is used to prove some simple arithmetic problem which are a==b, a>=b, a<=b; Besides it - * can be used to prove that a>=b or a<=b by knowing that c>=d or c<=d; + * This class is used to prove some simple arithmetic problem which are {@code a==b}, {@code a>=b}, + * {@code a<=b}; Besides it can be used to prove that {@code a>=b} or {@code a<=b} by + * knowing that {@code c>=d} or {@code c<=d;} * */ public class HandleArith { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java index 2030daafa5c..04d0c0b3483 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java @@ -25,9 +25,9 @@ /** * Term generator for inferring the range of values that a variable can have from a given non-linear - * (in)equation. The generator may only be called on formulas of the form v^n = l, - * v^n <= l, v^n >= l, where v is an atomic term (does not start with - * addition or multiplication) and l is a literal. The generator will then produce at most + * (in)equation. The generator may only be called on formulas of the form {@code v^n = l}, + * {@code v^n <= l}, {@code v^n >= l}, where {@code v} is an atomic term (does not start with + * addition or multiplication) and {@code l} is a literal. The generator will then produce at most * one formula that describes the solutions of the formula using linear (in)equations. */ public class RootsGenerator implements TermGenerator { diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java index 3f099a104a0..0d023fa3d02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java @@ -846,7 +846,7 @@ public static boolean equalsModBranchUniqueRenaming(SourceElement se1, SourceEle * The underlying idea is based upon the observation that many path conditions that should be * merged are conjunctions of mostly the same elements and, in addition, formulae phi and !phi * that vanish after creating the disjunction of the path conditions. The corresponding valid - * formula is (phi & psi) | (phi & !psi) <-> phi + * formula is {@code (phi & psi) | (phi & !psi) <-> phi} *

* * For formulae that cannot be simplified by this law, the method performs two additional @@ -1005,7 +1005,8 @@ public static void closeMergePartnerGoal(Node mergeNodeParent, Goal mergePartner } /** - * Converts a sequent (given by goal & pos in occurrence) to an SE state (U,C). Thereby, all + * Converts a sequent (given by {@link Goal} and {@link PosInOccurrence}) to an SE state (U,C). + * Thereby, all * program variables occurring in the symbolic state are replaced by branch-unique * correspondents in order to enable merging of different branches declaring local variables. *

@@ -1025,7 +1026,8 @@ public static SymbolicExecutionState sequentToSEPair(Node node, PosInOccurrence } /** - * Converts a sequent (given by goal & pos in occurrence) to an SE state (U,C,p). Thereby, all + * Converts a sequent (given by {@link Goal} and {@link PosInOccurrence}) to an SE state + * (U,C,p). Thereby, all * program variables occurring in the program counter and in the symbolic state are replaced by * branch-unique correspondents in order to enable merging of different branches declaring local * variables. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java index b132d5bd5ad..9410ea51e42 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java @@ -164,11 +164,11 @@ public void setBatchGoalStateChange(boolean value, Collection nodesToUpdat * Call this when the GUIProofTreeModel is no longer needed. GUIProofTreeModel registers a * Listener with its associated Proof object. This method unregisters that listener, which is a * good thing, as the proof maintains a reference to the listener, and the listener to the - * GUIProofTreeModel, so it would never become GC'ed unless you call this method. + * GUIProofTreeModel, so it would never become GCed unless you call this method. * *

* Note that after calling unregister, this GUIProofTreeModel does not respond to - * changes in the proof tree any more. + * changes in the proof tree anymore. */ public void unregister() { proof.removeProofTreeListener(proofTreeListener); @@ -180,7 +180,7 @@ public void register() { /** - * Sets whether this object should respond to changes in the the proof immediately. + * Sets whether this object should respond to changes in the proof immediately. */ public void setAttentive(boolean b) { LOGGER.debug("setAttentive: {}", b); @@ -199,7 +199,7 @@ public void setAttentive(boolean b) { } /** - * returns true if the model respond to changes in the proof immediately + * returns true if the model responds to changes in the proof immediately */ public boolean isAttentive() { return attentive; @@ -230,7 +230,7 @@ public void removeTreeModelListener(TreeModelListener l) { /** * - * @return whether or not {@link ProofTreeViewFilter#HIDE_CLOSED_SUBTREES} is active. + * @return whether {@link ProofTreeViewFilter#HIDE_CLOSED_SUBTREES} is active. */ public boolean hideClosedSubtrees() { return ProofTreeViewFilter.HIDE_CLOSED_SUBTREES.isActive(); @@ -239,7 +239,7 @@ public boolean hideClosedSubtrees() { /** * - * @return whether or not {@link ProofTreeViewFilter#HIDE_INTERACTIVE_GOALS} is active. + * @return whether {@link ProofTreeViewFilter#HIDE_INTERACTIVE_GOALS} is active. */ public boolean hideInteractiveGoals() { return ProofTreeViewFilter.HIDE_INTERACTIVE_GOALS.isActive(); @@ -277,13 +277,14 @@ public void setFilter(ProofTreeViewFilter filter, boolean active) { } /** - * Returns the child of parent at index index in the parent's child array. - * parent must be a node previously obtained from this data source. This should not - * return null if index is a valid index for parent (that is index >= 0 && - * index < getChildCount(parent)). + * Returns the child of {@code parent} at index {@code index} in the parent's child array. + * {@code parent} must be a node previously obtained from this data source. This should not + * return null if {@code index} is a valid index for {@code parent} (that is + * {@code index >= 0 && + * index < getChildCount(parent)}). * * @param parent a node in the tree, obtained from this data source - * @return the child of parent at index index + * @return the child of {@code parent} at index {@code index} */ @Override public Object getChild(Object parent, int index) { @@ -299,11 +300,12 @@ public Object getChild(Object parent, int index) { } /** - * Returns the number of children of parent. Returns 0 if the node is a leaf or if it has - * no children. parent must be a node previously obtained from this data source. + * Returns the number of children of {@code parent}. Returns 0 if the node is a leaf or if it + * has + * no children. {@code parent} must be a node previously obtained from this data source. * * @param parent a node in the tree, obtained from this data source - * @return the number of children of the node parent + * @return the number of children of the node {@code parent} */ @Override public int getChildCount(Object parent) { @@ -362,7 +364,7 @@ public boolean isLeaf(Object guiNode) { /** * Messaged when the user has altered the value for the item identified by path to - * newValue. We throw an exception, as proofs are not meant to be chaged via the JTree + * newValue. We throw an exception, as proofs are not meant to be changed via the JTree * editing facility. * * @param path path to the node that the user has altered. @@ -468,7 +470,7 @@ protected void fireTreeStructureChanged(Object[] path) { } // caches for the GUIProofTreeNode and GUIBranchNode objects - // generated to represent the nodes resp. subtrees of the Proof. + // generated to represent the nodes and subtrees of the proof. private WeakHashMap proofTreeNodes = new WeakHashMap<>(); @@ -504,7 +506,7 @@ public GUIBranchNode findBranch(Node n) { /** * Return the GUIBranchNode corresponding to the subtree rooted at n. Generate one if necessary, - * using label as the the subtree label. + * using label as the subtree label. */ public GUIBranchNode getBranchNode(Node n, Object label) { GUIBranchNode res = findBranch(n); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index 5e67068106d..4fbc7ecf688 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -269,14 +269,18 @@ protected JTextField addTextField(String title, String text, String info, /** * Create a titled JSpinner (with additional information) for entering numbers in [min, max]. - * The min and max values have to be comparable (to check min <= value <= max) and min must be a - * Number to be handled by the JSpinner's SpinnerNumberModel correctly. The Number class of min - * also determines how the default NumberFormatter used by the JSpinner formats entered Strings + * The min and max values have to be comparable (to check {@code min <= value <= max} and + * {@code min} must be a + * {@link Number} to be handled by the {@link JSpinner}'s {@link SpinnerNumberModel} correctly. + * The Number class of min + * also determines how the default {@link javax.swing.text.NumberFormatter} used by the + * {@link JSpinner} formats entered Strings * (see {@link javax.swing.text.NumberFormatter#stringToValue(String)}). * * If there are additional restrictions for the entered values, the passed validator can check - * those. The entered values have to be of a subclass of Number (as this is a number text - * field), otherwise the Number-Validator will fail. + * those. The entered values have to be of a subclass of {@link Number} (as this is a number + * text + * field), otherwise the {@link Validator} will fail. * * @param title the title of the text field * @param min the minimum value that can be entered diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java index b902f17915f..2181760ca64 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java @@ -8,8 +8,8 @@ import org.key_project.util.Strings; /** - * This class implements ImmMap and provides a persistent Map. It is a simple implementation - * like lists + * This class implements {@code ImmutableMap} and provides a persistent map. + * It is a simple implementation like lists */ public class DefaultImmutableMap implements ImmutableMap { @@ -72,12 +72,14 @@ protected DefaultImmutableMap(ImmutableMapEntry entry, DefaultImmutableMap /** - * inserts mapping into the map (old map is not modified) if key exists old entry has + * inserts mapping {@code } into the map (old map is not modified) if key exists old + * entry has * to be removed {@code null} is not allowed for key or value. * * @param key a S to be used as key * @param value a T to be stored as value - * @return a ImmMap including the pair and all other pairs of the current map + * @return a ImmutableMap including the {@code }-pair and all other pairs of the + * current map * with keys different from the given key */ public ImmutableMap put(S key, T value) { diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java index 7ec4a4c30a6..fe8b3bd499d 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java @@ -13,7 +13,8 @@ public interface ImmutableMap extends Iterable>, java.io.Serializable { /** - * adds a mapping to the Map (old map is not modified) if key exists old entry has to + * adds a mapping {@code } to the Map (old map is not modified) if key exists old entry + * has to * be removed * * @return the new mapping diff --git a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java index b3e87321633..3786540c13d 100644 --- a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java @@ -156,11 +156,13 @@ public static String removeTags(String text) { * The following signs are replaced: * * 

-     * " => "quot;
-     * & => "amp;
-     * ' => "apos;
-     * < => "lt;
-     * > => "gt;
+     * {@code
+     * " => ""
+     * & => "&
+     * ' => "'
+     * < => "<
+     * > => ">
+     * }
      *
*

* diff --git a/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java b/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java index 66e6d26593d..d8b75b0ac66 100644 --- a/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java +++ b/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java @@ -26,7 +26,7 @@ * should be used instead: *
    *
  • {@link #getClassforName(String)} instead of {@link Class#forName(String)}
    • - *
  • {@link #loadServices(Class, Class) instead of {@link ServiceLoader#load(Class)}
    • + *
  • {@link #loadServices(Class, Class)} instead of {@link ServiceLoader#load(Class)}
    • *
*

* The application specific behavior is implemented in {@link IClassLoader} instances. The used diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java b/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java index 8a2c9027d8a..7c4d7ef3ec6 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java @@ -31,12 +31,22 @@ * Adding formulas to the antecedent: '==> p' as goal node and adding q to the antecedent results in * two branches: *

- * 1) q ==> p 2) ==> p,q <-- this branch is set to interactive such that the automatic strategies do - * not expand it Adding formulas to the succedent: '==> p' as goal node and adding q to the + *

    + *
  1. {@code q ==> p}
    2. + *
  2. {@code ==> p,q} {@code <--} this branch is set to interactive such that the automatic + * strategies do + * not expand it.
    3. + *
+ * Adding formulas to the succedent: '==> p' as goal node and adding q to the * succedent results in two branches: + * *

- * 1) q ==> p <-- this branch is set to interactive such that the automatic strategies do not expand - * it 2) ==> p,q + *

    + *
  1. {@code q ==> p} {@code <--} this branch is set to interactive such that the automatic + * strategies do not expand + * it
    2. + *
  2. {@code ==> p,q}
    3. + *
* * @author Sarah Grebing * @author Alexander Weigl diff --git a/recoder/src/main/java/recoder/io/ArchiveDataLocation.java b/recoder/src/main/java/recoder/io/ArchiveDataLocation.java index 042ad5c7a7d..e85768a4f0b 100644 --- a/recoder/src/main/java/recoder/io/ArchiveDataLocation.java +++ b/recoder/src/main/java/recoder/io/ArchiveDataLocation.java @@ -70,9 +70,12 @@ public ZipFile getFile() { } /** - * returns a URL-like string representation of the location in the form " : - * ", i.e. file:/bin/sh url:http://mywww/myfile - * archive:recoder.zip:recoder/java/JavaProgramFactory.class + * returns a URL-like string representation of the location in the form {@code : + * }, i.e. + * + * 
+     * {@code  file:/bin/sh url:http://mywww/myfile archive:recoder.zip:recoder/java/JavaProgramFactory.class}
+     *
*/ public String toString() { return getType() + ":" + archiveFile.getName() + "?" + itemName; diff --git a/recoder/src/main/java/recoder/io/DataFileLocation.java b/recoder/src/main/java/recoder/io/DataFileLocation.java index 0432bd0b407..f55352b4224 100644 --- a/recoder/src/main/java/recoder/io/DataFileLocation.java +++ b/recoder/src/main/java/recoder/io/DataFileLocation.java @@ -54,9 +54,16 @@ private void setFile(File f) { } /** - * returns a URL-like string representation of the location in the form " : - * ", i.e. file:/bin/sh url:http://mywww/myfile - * zip:recoder.zip:recoder/java/JavaProgramFactory.class + * returns a URL-like string representation of the location in the form + * + * 
+     * {@code
+     * :"
+     * },
+     *
+ * + * i.e. + * {@code file:/bin/sh url:http://mywww/myfile zip:recoder.zip:recoder/java/JavaProgramFactory.class} */ public String toString() { return getType() + ":" + file.getPath(); diff --git a/recoder/src/main/java/recoder/io/DataLocation.java b/recoder/src/main/java/recoder/io/DataLocation.java index 42baef02770..9de7ba71dc7 100644 --- a/recoder/src/main/java/recoder/io/DataLocation.java +++ b/recoder/src/main/java/recoder/io/DataLocation.java @@ -23,9 +23,13 @@ public interface DataLocation { String getType(); /** - * returns a URL-like string representation of the location in the form " : - * ", i.e. file:/bin/sh url:http://mywww/myfile + * returns a URL-like string representation of the location in the form + * + * 
+     * {@code  : ", i.e. file:/bin/sh url:http://mywww/myfile
      * zip:recoder.zip:recoder/java/JavaProgramFactory.class
+     * }
+     *
*/ String toString(); diff --git a/recoder/src/main/java/recoder/io/PropertyNames.java b/recoder/src/main/java/recoder/io/PropertyNames.java index 497d0088aef..338a636e444 100644 --- a/recoder/src/main/java/recoder/io/PropertyNames.java +++ b/recoder/src/main/java/recoder/io/PropertyNames.java @@ -128,27 +128,27 @@ public interface PropertyNames { * * * 
-     * 

+     * {@code
      * while (i < n) { if (a[i] == x) { return i; } i += 1; }
-     *
+     * }
      *
* * * * * 
-     * 

+     * {@code
      * while (i < n) { if (a[i] == x) { return i; } i += 1; }
-     *
+     * }
      *
* * * * * 
-     * 

+     * {@code
      * while (i < n) { if (a[i] == x) { return i; } i += 1; }
-     *
+     * }
      *
* * @@ -409,16 +409,16 @@ public interface PropertyNames { * * * 
-     * 

+     * {@code
      * (1 < < 3)
-     *
+     * }
      *
* * * * * 
-     * ( 1 < < 3 )
+     * {@code ( 1 < < 3 ) }
      *
* * diff --git a/recoder/src/main/java/recoder/java/PackageSpecification.java b/recoder/src/main/java/recoder/java/PackageSpecification.java index 927078430db..af7c05d8ba9 100644 --- a/recoder/src/main/java/recoder/java/PackageSpecification.java +++ b/recoder/src/main/java/recoder/java/PackageSpecification.java @@ -165,7 +165,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. * @throws ClassCastException if the new child cannot take over the role of the old one. */ diff --git a/recoder/src/main/java/recoder/java/ProgramElement.java b/recoder/src/main/java/recoder/java/ProgramElement.java index 39f83f8dd1d..164b138adad 100644 --- a/recoder/src/main/java/recoder/java/ProgramElement.java +++ b/recoder/src/main/java/recoder/java/ProgramElement.java @@ -52,7 +52,7 @@ public interface ProgramElement extends SourceElement, ModelElement { /** * Set comments. * - * @param c a comment list. + * @param list a comment list. */ void setComments(ASTList list); diff --git a/recoder/src/main/java/recoder/java/declaration/ParameterDeclaration.java b/recoder/src/main/java/recoder/java/declaration/ParameterDeclaration.java index 87b7deac5b4..52bec9bde62 100644 --- a/recoder/src/main/java/recoder/java/declaration/ParameterDeclaration.java +++ b/recoder/src/main/java/recoder/java/declaration/ParameterDeclaration.java @@ -12,7 +12,8 @@ import recoder.list.generic.ASTList; /** - * 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). */ diff --git a/recoder/src/main/java/recoder/java/expression/operator/New.java b/recoder/src/main/java/recoder/java/expression/operator/New.java index 8ff663698df..7c07de91bda 100644 --- a/recoder/src/main/java/recoder/java/expression/operator/New.java +++ b/recoder/src/main/java/recoder/java/expression/operator/New.java @@ -19,12 +19,22 @@ * The object allocation operator. There are two variants for New: *
    *
  1. Class constructor call
    - * new XYZ(a1, ..., an)
    - * if getType() instanceof UserType + * + * 
    + * {@code
+ *  new XYZ(a_1, ..., a_n)
+ *  if getType() instanceof UserType
+ * }
+ *
    + * *
  2. Anonymous Inner Class definition and construction
    - * new XYZ(a1, ..., an) - * { m1, ..., mk }
    - * if getType() instanceof UserType && getClassDeclaration() !=null + * {@code new XYZ(a_1, ..., a_n)} + * + * 
    + * @code{  m_1, ..., m_k
+ * if getType() instanceof UserType && getClassDeclaration() != null
+ * }
+ *
    *
* The access path is null in most cases, except when an inner class constructor is invoked * from an outer instance. diff --git a/recoder/src/main/java/recoder/java/reference/SpecialConstructorReference.java b/recoder/src/main/java/recoder/java/reference/SpecialConstructorReference.java index b0b3025c199..cce27521f8c 100644 --- a/recoder/src/main/java/recoder/java/reference/SpecialConstructorReference.java +++ b/recoder/src/main/java/recoder/java/reference/SpecialConstructorReference.java @@ -156,7 +156,7 @@ public Expression getExpressionAt(int index) { * 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. * @throws ClassCastException if the new child cannot take over the role of the old one. */ diff --git a/recoder/src/main/java/recoder/java/statement/LoopStatement.java b/recoder/src/main/java/recoder/java/statement/LoopStatement.java index 5a383be4923..87e76ea582a 100644 --- a/recoder/src/main/java/recoder/java/statement/LoopStatement.java +++ b/recoder/src/main/java/recoder/java/statement/LoopStatement.java @@ -217,7 +217,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. * @throws ClassCastException if the new child cannot take over the role of the old one. */ diff --git a/recoder/src/main/java/recoder/java/statement/Switch.java b/recoder/src/main/java/recoder/java/statement/Switch.java index 2283a3d2572..d4a9c582ad6 100644 --- a/recoder/src/main/java/recoder/java/statement/Switch.java +++ b/recoder/src/main/java/recoder/java/statement/Switch.java @@ -198,7 +198,7 @@ public void makeParentRoleValid() { * 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. * @throws ClassCastException if the new child cannot take over the role of the old one. */ diff --git a/recoder/src/main/java/recoder/util/Equality.java b/recoder/src/main/java/recoder/util/Equality.java index 9a2b9baa5ba..bf59e00c8e9 100644 --- a/recoder/src/main/java/recoder/util/Equality.java +++ b/recoder/src/main/java/recoder/util/Equality.java @@ -8,12 +8,12 @@ * This interface defines an equality relation between two objects. Equality relations are *
    *
  • reflexive
    - * equals(x, x)
    • + * equals(x, x) *
  • symmetric
    - * equals(x, y) == equals(y, x)
    • + * {@code equals(x, y) == equals(y, x)} *
  • transitive
    - * (equals(x, y) && equals(y, z)) implies - * equals(x, z)
    • + * {@code (equals(x, y) && equals(y, z))} implies + * {@code equals(x, z)} *
* Whether or not objects of different type or null objects are allowed is up to the * specific implementation. @@ -29,7 +29,7 @@ public interface Equality { Equality NATURAL = Order.NATURAL; /** * Identity equality relation object. The implementation compares x and y for object identity - * (x == y). Two null objects are considered equal. + * (x == y). Two null objects are considered equal. */ Equality IDENTITY = Order.IDENTITY; diff --git a/recoder/src/main/java/recoder/util/Order.java b/recoder/src/main/java/recoder/util/Order.java index 11ff1adbac9..4e08c45fd04 100644 --- a/recoder/src/main/java/recoder/util/Order.java +++ b/recoder/src/main/java/recoder/util/Order.java @@ -22,22 +22,28 @@ * isComparable(x, y) implies * less(x, y) || less(y, x) * - * As both relations are related by
- * lessOrEquals(x, y) == (less(x, y) || equals(x, y)) - * ,
this interface extends an equality relation. + * As both relations are related by + * + * 
+ * {@code
+ * lessOrEquals(x,y)==(less(x,y) || equals(x,y))}
+ * ,
+ *
+ * + * this interface extends an equality relation. *

* The usual way is to calculate all relations at once and returning a status code such as * int compareTo(x, y). However, this function alone can not capture partial orders and * is not efficient if the single comparisons become costly - see for instance the subset relation. - * The prize to pay for the more explicite interface is a slight code overhead, but this should not - * lead to a noticeable loss of performance. And of course, lessOrEquals(x, y) - * should be a bit more comprehensible than compareTo(x, y)  <= 0. + * The prize to pay for the more explicit interface is a slight code overhead, but this should not + * lead to a noticeable loss of performance. And of course, {@code lessOrEquals(x,y)} + * should be a bit more comprehensible than {@code compareTo(x,y) <= 0}. * *

- * Whether or not objects of different type or null objects are allowed is up to the - * specific implementation. This isComparable - * predicate should be defined for all objects. The orders are total, if the predicate - * yields true for any input - with the possible exception of null objects. If two + * Whether objects of different type or {@code null} objects are allowed is up to the + * specific implementation. This {@code isComparable} + * predicate should be defined for all objects. The orders are total, if the predicate + * yields true for any input - with the possible exception of {@code null} objects. If two * objects are not comparable, the result of the other predicates is not defined unless stated * explicitely. * From 5c2b01410e0d4e1918e9e8b0bfd04246014f9250 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 30 Oct 2023 12:09:26 +0100 Subject: [PATCH 2/6] Fixes from review --- .../key/symbolic_execution/SymbolicLayoutExtractor.java | 6 ++---- .../key/symbolic_execution/po/ProgramMethodSubsetPO.java | 3 +-- .../src/main/java/de/uka/ilkd/key/logic/op/Equality.java | 2 +- .../src/main/java/recoder/java/expression/operator/New.java | 2 +- recoder/src/main/java/recoder/util/Equality.java | 4 ++-- 5 files changed, 7 insertions(+), 10 deletions(-) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java index 51a53013ff4..510334392db 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java @@ -44,8 +44,7 @@ * Example program: * * 

- * {
- *     @code
+ * {@code
  *     public class Example {
  *         private int value;
  *
@@ -69,8 +68,7 @@
  * The following code snippet shows how to use this class:
  *
  * 
- * {
- *     @code
+ * {@code
  *     SymbolicLayoutExtractor e = new SymbolicLayoutExtractor(node);
  *     e.analyse();
  *     for (int i = 0; i < e.getLayoutsCount(); i++) {
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java
index ba8232f5f3e..7177cf5e1c7 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java
@@ -41,8 +41,7 @@
  * Imagine the following snippet:
  *
  * 
- * {
- *     @code
+ * {@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
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
index 89b5f6c6b7e..bae8c6beeda 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
@@ -8,7 +8,7 @@
 
 
 /**
- * This class defines the equality operator {@code ==}. It is a binary predicate accepting arbitrary
+ * This class defines the logic equality operator {@code =}. It is a binary predicate accepting arbitrary
  * terms
  * (sort "any") as arguments.
  *
diff --git a/recoder/src/main/java/recoder/java/expression/operator/New.java b/recoder/src/main/java/recoder/java/expression/operator/New.java
index 7c07de91bda..fdbb7b02810 100644
--- a/recoder/src/main/java/recoder/java/expression/operator/New.java
+++ b/recoder/src/main/java/recoder/java/expression/operator/New.java
@@ -31,7 +31,7 @@
  * {@code new XYZ(a_1, ..., a_n)}
  *
  * 
- * @code{  m_1, ..., m_k
+ * {@code{  m_1, ..., m_k
  * if getType() instanceof UserType && getClassDeclaration() != null
  * }
  * 

diff --git a/recoder/src/main/java/recoder/util/Equality.java b/recoder/src/main/java/recoder/util/Equality.java
index bf59e00c8e9..f325ca7e93d 100644
--- a/recoder/src/main/java/recoder/util/Equality.java
+++ b/recoder/src/main/java/recoder/util/Equality.java
@@ -15,7 +15,7 @@
  * {@code (equals(x, y) && equals(y, z))} implies
  * {@code  equals(x, z)}
  * 
- * Whether or not objects of different type or null objects are allowed is up to the
+ * Whether objects of different type or null objects are allowed is up to the
  * specific implementation.
  *
  * @author AL
@@ -23,7 +23,7 @@
 public interface Equality {
 
     /**
-     * Natural equality relation object. The implementation calls x.equals(y), hence no
+     * Natural equality relation object. The implementation calls {@code x.equals(y)}, hence no
      * null are allowed (not even for y, as the relation must be symmetric).
      */
     Equality NATURAL = Order.NATURAL;

From c9b85f62e8e025d2f3ef5bd566cbb4ab41824e5d Mon Sep 17 00:00:00 2001
From: unp1 
Date: Mon, 30 Oct 2023 12:14:27 +0100
Subject: [PATCH 3/6] Apply suggestions from code review

Suggestions from reviewers

Co-authored-by: Arne Keller 
Co-authored-by: Daniel Drodt <132357467+Drodt@users.noreply.github.com>
---
 .../main/java/de/uka/ilkd/key/logic/op/SubstOp.java    |  2 +-
 .../de/uka/ilkd/key/speclang/WellDefinednessCheck.java |  2 +-
 .../main/java/org/key_project/util/java/XMLUtil.java   | 10 +++++-----
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
index c4107835584..007b11c4f2f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
@@ -46,7 +46,7 @@ public Sort sort(ImmutableArray terms) {
      * @throws TermCreationException if the check fails
      */
     @Override
-    protected void additionalValidTopLevel(Term term) {
+    protected void additionalValidTopLevel(Term term) throws TermCreationException {
         if (term.varsBoundHere(1).size() != 1) {
             throw new TermCreationException(this, term);
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
index 8a5f53edea1..5517964de1a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
@@ -916,7 +916,7 @@ public static boolean isOn() {
 
     /**
      * collects terms for precondition, assignable clause and other specification elements, and
-     * {code postcondition {@code &} signals-clause}
+     * postcondition and signals-clause
      */
     public final POTerms createPOTerms() {
         final Condition pre = this.getRequires();
diff --git a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java
index 3786540c13d..78aa587411c 100644
--- a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java
+++ b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java
@@ -157,11 +157,11 @@ public static String removeTags(String text) {
      *
      * 
      * {@code
-     * " => ""
-     * & => "&
-     * ' => "'
-     * < => "<
-     * > => ">
+     * " => "
+     * & => &
+     * ' => '
+     * < => <
+     * > => >
      * }
      * 

      * 


From 3ef9ff7960f1067926007cef0935e761b36650c7 Mon Sep 17 00:00:00 2001
From: Richard Bubel 
Date: Mon, 30 Oct 2023 12:24:56 +0100
Subject: [PATCH 4/6] Replaced other erroneous instances of @

---
 .../key/java/CreateArrayMethodBuilder.java    | 20 ++++++++---------
 .../ilkd/key/macros/scripts/meta/Flag.java    |  6 ++---
 .../de/uka/ilkd/key/rule/TacletMatcher.java   |  8 +++----
 .../main/java/recoder/convenience/Format.java | 17 +++++++-------
 .../java/recoder/convenience/Formats.java     | 22 +++++++++----------
 5 files changed, 37 insertions(+), 36 deletions(-)

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java
index 6ba1bf9dc8c..b89f3443a8f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java
@@ -252,18 +252,18 @@ private StatementBlock getCreateArrayBody(
     }
 
     /**
-     * creates the body of method <createArrayHelper(int
-     * paramLength)> therefore it first adds the statements responsible to take the
+     * creates the body of method {@code } 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
-     * <prepare>() setting the arrays fields on their default value.
+     * {@code ()} setting the arrays fields on their default value.
      *
-     * @param length the final public ProgramVariable length of the array
-     * @param fields the IList of the current array
-     * @param createTransient a boolean indicating if a transient array has
+     * @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 


-     *     
+     * @param transientType a ProgramVariable identifying the kind of transient
+     * @return the StatementBlock which is the method's body 


+     *  
 {@code
      *  {
      *    this. = this..;
      *    this. = false;
@@ -273,7 +273,7 @@ private StatementBlock getCreateArrayBody(
      *    this. = true;
      *    return this;
      *   }
-     *   
+     *   }

      */
     private StatementBlock getCreateArrayHelperBody(
             ProgramVariable length,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java
index 6567bbb4625..dac84449ac1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java
@@ -9,10 +9,10 @@
  * Used to mark flag for proof script commands. For example "instantitate formula='...' ... hide" is
  * denoted as
  * 

- * 
- * @Flag(name="hide"}
+ * 
{@code
+ * @Flag(name="hide"}
  * boolean hideFormula.
- * 

+ * }

  * 

  * Only applicable to boolean fields!
  *
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java
index 3f22169430a..b03c4744c6f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java
@@ -72,13 +72,13 @@ MatchConditions checkVariableConditions(SchemaVariable var,
      * matches the given term against the taclet's find term if the taclet has no find term or the
      * match is unsuccessful null
      * is returned
-     * @param term the Term to be matched against the find expression
+     * @param term the Term to be matched against the find expression
      * of the taclet
-     * @param matchCond the MatchConditions with side conditions to be
-     * satisfied, eg. partial instantiations of schema variables; before
+     * @param matchCond the MatchConditions with side conditions to be
+     * satisfied, e.g. partial instantiations of schema variables; before
      * calling this method the constraint contained in the match conditions
      * must be ensured to be satisfiable, i.e.
-     *        matchCond.getConstraint ().isSatisfiable ()  must return true
+     *       {@code matchCond.getConstraint().isSatisfiable()} must return true
      *
      * @param services the Services
      * @return the found schema variable mapping or null if the matching failed
diff --git a/recoder/src/main/java/recoder/convenience/Format.java b/recoder/src/main/java/recoder/convenience/Format.java
index 7fdfc062437..730ea80186c 100644
--- a/recoder/src/main/java/recoder/convenience/Format.java
+++ b/recoder/src/main/java/recoder/convenience/Format.java
@@ -329,11 +329,12 @@ public static String toString(String formatText, String header, String separator
     }
 
     /**
-     * Formats a source element using a default format. The default format string is "\"%s\"
+     * Formats a source element using a default format.
+     * The default format string is {@code "\"%s\"@%p [%f]"}
+     *
+     * @param se the source element to be formatted.
+     * @return a textual representation of the source element.
      *
-     * @param se the source element to be formatted.
-     * @return a textual representation of the source element.
-     * @%p [%f]".
      */
     public static String toString(ProgramElement se) {
         return toString("\"%s\" @%p [%f]", se);
@@ -341,11 +342,11 @@ public static String toString(ProgramElement se) {
 
     /**
      * Formats a program element list using a default format. The default format string is
-     * "\"%s\"
+     * {@code "\"%s\" @%p"}
+     *
+     * @param l the list to be formatted.
+     * @return a textual representation of the list.
      *
-     * @param l the list to be formatted.
-     * @return a textual representation of the list.
-     * @%p".
      */
     public static String toString(List l) {
         return toString("\"%s\" @%p", l);
diff --git a/recoder/src/main/java/recoder/convenience/Formats.java b/recoder/src/main/java/recoder/convenience/Formats.java
index 3d3f57acc56..33a43bfcd40 100644
--- a/recoder/src/main/java/recoder/convenience/Formats.java
+++ b/recoder/src/main/java/recoder/convenience/Formats.java
@@ -13,27 +13,27 @@ public interface Formats {
 
     /**
      * Long default formatting string for program elements, handsome for descriptive external error
-     * messages. Derives messages such as 
-     * MethodReference "x.f(i + 1)"
-     *
-     * @23/45 in FILE:/tmp/Foo.java.
+     * messages. Derives messages such as
+     * 
+     * {@code
+     * MethodReference "x.f(i + 1)" @23/45 in FILE:/tmp/Foo.java
+     * }

      */
     String ELEMENT_LONG = "%c \"%s\" @%p in \"%f\"";
 
     /**
      * Long formatting string for program elements, omitting file information. Derives messages such
-     * as MethodReference "x.f(i + 1)"
-     *
-     * @23/45.
+     * as 
{@code
+     * MethodReference "x.f(i + 1)" @23/45}

      */
     String ELEMENT_LONG_LOCAL = "%c \"%s\" @%p";
 
     /**
      * Short default formatting string for named program elements, handsome for descriptive external
-     * error messages. Derives messages such as 
-     * MethodDeclaration "Foo.f(int)"
-     *
-     * @23/45 in FILE:/tmp/Foo.java.
+     * error messages. Derives messages such as
+     * 
{@code
+     * MethodDeclaration "Foo.f(int)"@23/45 in FILE:/tmp/Foo.java
+     * }

      */
     String ELEMENT_SHORT = "%c \"%N\" @%p in \"%f\"";
 }

From 552f06a964a4067204fee1ded004af3eb6c5951c Mon Sep 17 00:00:00 2001
From: Richard Bubel 
Date: Mon, 30 Oct 2023 13:11:59 +0100
Subject: [PATCH 5/6] More fixes and polishing (spotlessApply turns some @ to
 their encoding number; for those comments it is switched off)

---
 .../key/util/rifl/SpecificationEntity.java    |  4 +--
 .../SymbolicLayoutExtractor.java              |  8 +++--
 .../po/ProgramMethodSubsetPO.java             |  6 +++-
 .../key/java/CreateArrayMethodBuilder.java    | 12 ++++---
 .../de/uka/ilkd/key/logic/op/Equality.java    |  8 ++---
 .../ilkd/key/macros/scripts/meta/Flag.java    | 17 ++++++---
 .../de/uka/ilkd/key/rule/TacletMatcher.java   | 36 ++++++++++---------
 .../exploration/ui/ExplorationStepsList.java  |  5 ++-
 .../main/java/recoder/convenience/Format.java |  4 +--
 .../java/recoder/convenience/Formats.java     | 19 +++++++---
 .../recoder/java/expression/operator/New.java | 17 +++++----
 .../reference/EnumConstructorReference.java   |  2 +-
 .../recoder/service/DefaultSourceInfo.java    | 10 +++---
 13 files changed, 92 insertions(+), 56 deletions(-)

diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java
index edf71a354df..b472160ddaa 100644
--- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java
+++ b/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);
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java
index 510334392db..7159ac796c2 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java
+++ b/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
 /**
  * 

  * Instances of this class can be used to compute memory layouts (objects with values and
@@ -41,7 +43,7 @@
  * started. Such memory layouts are named initial memory layouts.
  * 

  * 

- * Example program:
+ * Example program:

  *
  * 
  * {@code
@@ -59,6 +61,8 @@
  * }
  * 

  *
+ * 

+ * 

  * 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
@@ -78,7 +82,6 @@
  *     }
  * }
  * 

- * 

  * 

  * 

  * Rough description of the implemented algorithm:
@@ -129,6 +132,7 @@
  * @see ISymbolicLayout
  * @see ExecutionNodeSymbolicLayoutExtractor
  */
+// spotless:on
 public class SymbolicLayoutExtractor extends AbstractUpdateExtractor {
     /**
      * The used {@link IModelSettings}.
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java
index 7177cf5e1c7..1405ff15f6c 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java
+++ b/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
 /**
  * 

  * This proof obligation executes selected statements of the body of a given {@link IProgramMethod}.
@@ -47,7 +49,8 @@
  *     int z = 3; // from 5/16 to 6/16
  * }
  *
- * + *

+ *

* 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. @@ -77,6 +80,7 @@ * * @author Martin Hentschel */ +//spotless:on public class ProgramMethodSubsetPO extends ProgramMethodPO { /** * Contains all undeclared variables used in the method part to execute. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java index b89f3443a8f..32567dd0107 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java @@ -260,10 +260,13 @@ private StatementBlock getCreateArrayBody( * @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) + * 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

- * 

 {@code
+     * @return the StatementBlock which is the method's body 

+     *         

+     *
+     *         
+     *  {@code
      *  {
      *    this. = this..;
      *    this. = false;
@@ -273,7 +276,8 @@ private StatementBlock getCreateArrayBody(
      *    this. = true;
      *    return this;
      *   }
-     *   }

+     *   }
+     *
*/ private StatementBlock getCreateArrayHelperBody( ProgramVariable length, diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java index bae8c6beeda..432abdb9806 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java @@ -8,13 +8,11 @@ /** - * This class defines the logic equality operator {@code =}. 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 {@code <->} (which could alternatively be seen - * as a - * Junctor). + * as a Junctor). */ public final class Equality extends AbstractSortedOperator { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java index dac84449ac1..42705d5789d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/Flag.java @@ -3,23 +3,32 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts.meta; +// Need to switch spotless off for the comment because it replaces @Flag with @Flag +// spotless:off /** * Currently not implemented in {@link ArgumentsLifter} *

* Used to mark flag for proof script commands. For example "instantitate formula='...' ... hide" is * denoted as + *

*

- * 

{@code
- * @Flag(name="hide"}
- * boolean hideFormula.
- * }
+ * + * 
+ * {@code
+ *  @Flag(name="hide"}
+ *  boolean hideFormula.
+ * }
+ *
+ *

*

* Only applicable to boolean fields! + *

* * @author Alexander Weigl * @version 1 (21.04.17) * @see Option */ +//spotless:on public @interface Flag { /** * Name of the command line argument. diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java index b03c4744c6f..27671e8bbb8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java @@ -14,16 +14,18 @@ public interface TacletMatcher { /** - * Match the given template (which is probably a formula of the if sequence) against a list of + * Match the given template (which is probably a formula of the assumes-sequent) against a list + * of * constraint formulas (probably the formulas of the antecedent or the succedent), starting with - * the given instantiations and constraint p_matchCond. + * the given instantiations and constraint {@code p_matchCond}. * * @param p_toMatch list of constraint formulas to match p_template to * @param p_template template formula as in "match" * @param p_matchCond already performed instantiations * @param p_services the Services object encapsulating information about the java datastructures * like (static)types etc. - * @return Two lists (in an IfMatchResult object), containing the the elements of p_toMatch that + * @return Two lists (in an {@link IfMatchResult} object), containing the elements of + * {@code p_toMatch} that * could successfully be matched against p_template, and the corresponding * MatchConditions. */ @@ -31,9 +33,12 @@ IfMatchResult matchIf(ImmutableList p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services); /** - * Match the whole if sequent using the given list of instantiations of all if sequent formulas, - * starting with the instantiations given by p_matchCond. PRECONDITION: p_toMatch.size () == - * ifSequent ().size () + * Match the whole if sequent using the given list of instantiations of all assumes-sequent + * formulas, + * starting with the instantiations given by p_matchCond. + *

+ * PRECONDITION: {@code p_toMatch.size () == ifSequent().size()} + *

* * @return resulting MatchConditions or null if the given list p_toMatch does not match */ @@ -70,18 +75,19 @@ MatchConditions checkVariableConditions(SchemaVariable var, /** * matches the given term against the taclet's find term if the taclet has no find term or the - * match is unsuccessful null + * match is unsuccessful null * is returned + * * @param term the Term to be matched against the find expression - * of the taclet + * of the taclet * @param matchCond the MatchConditions with side conditions to be - * satisfied, e.g. partial instantiations of schema variables; before - * calling this method the constraint contained in the match conditions - * must be ensured to be satisfiable, i.e. - * {@code matchCond.getConstraint().isSatisfiable()} must return true + * satisfied, e.g. partial instantiations of schema variables; before + * calling this method the constraint contained in the match conditions + * must be ensured to be satisfiable, i.e. + * {@code matchCond.getConstraint().isSatisfiable()} must return true * * @param services the Services - * @return the found schema variable mapping or null if the matching failed + * @return the found schema variable mapping or null if the matching failed */ MatchConditions matchFind(Term term, MatchConditions matchCond, Services services); @@ -109,7 +115,7 @@ MatchConditions matchSV(SchemaVariable sv, Term term, MatchConditions matchCond, * {@link MatchConditions} {@code matchCond} * * @param sv the {@link SchemaVariable} - * @param pe the {@link ProgramElement} as a candidate for instantition of {@code sv} + * @param pe the {@link ProgramElement} as a candidate for instantiation of {@code sv} * @param matchCond the {@link MatchConditions} with additional constraints that need to be * considered * @param services the {@link Services} @@ -118,6 +124,4 @@ MatchConditions matchSV(SchemaVariable sv, Term term, MatchConditions matchCond, */ MatchConditions matchSV(SchemaVariable sv, ProgramElement pe, MatchConditions matchCond, Services services); - - } diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java b/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java index 4beb188f012..cfc68cf0b41 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java @@ -130,9 +130,8 @@ private List collectAllExplorationSteps(Node root, DefaultTreeModel dtm, * During collection of the nodes, the nodes are grouped in the given TreeModel {@code dtm} *

* - * @param n start node of exploration indow, KeYMediator mediator) { if (leftPanel == null) - * leftPanel = new ExplorationStepsList(window); return Collections.singleton(leftPanel); - * }* @param foundNodes filled with found exploration nodes + * @param node start node of exploration + * @param foundNodes filled with found exploration nodes * @param dtm a tree model which is filled with nodes * @param parent the corresponding entry of {@code n} in the tree model */ diff --git a/recoder/src/main/java/recoder/convenience/Format.java b/recoder/src/main/java/recoder/convenience/Format.java index 730ea80186c..a6997e6e1db 100644 --- a/recoder/src/main/java/recoder/convenience/Format.java +++ b/recoder/src/main/java/recoder/convenience/Format.java @@ -285,13 +285,13 @@ private static void append(Position pos, int columns, StringBuffer buf) { /** * Formats a list of model elements. Each element is formatted according to the format string by - * a call to {@link #toString(String, String, String, String, ModelElementList)}using + * a call to {@link #toString(String, String, String, String, List)} using * "(", ", ", ")" formatting. * * @param formatText the format text, containing tags. * @param l the list to be formatted. * @return a textual representation of the list. - * @see #toString(String, String, String, String, ModelElementList) + * @see #toString(String, String, String, String, List) */ public static String toString(String formatText, List l) { return toString(formatText, "(", ", ", ")", l); diff --git a/recoder/src/main/java/recoder/convenience/Formats.java b/recoder/src/main/java/recoder/convenience/Formats.java index 33a43bfcd40..1aaf8eb9433 100644 --- a/recoder/src/main/java/recoder/convenience/Formats.java +++ b/recoder/src/main/java/recoder/convenience/Formats.java @@ -14,26 +14,35 @@ public interface Formats { /** * Long default formatting string for program elements, handsome for descriptive external error * messages. Derives messages such as + * * 
      * {@code
      * MethodReference "x.f(i + 1)" @23/45 in FILE:/tmp/Foo.java
-     * }
+ * } + * */ String ELEMENT_LONG = "%c \"%s\" @%p in \"%f\""; /** * Long formatting string for program elements, omitting file information. Derives messages such - * as 
{@code
-     * MethodReference "x.f(i + 1)" @23/45}
+ * as + * + * 
+     * {@code
+     * MethodReference "x.f(i + 1)" @23/45}
+     *
*/ String ELEMENT_LONG_LOCAL = "%c \"%s\" @%p"; /** * Short default formatting string for named program elements, handsome for descriptive external * error messages. Derives messages such as - * 
{@code
+     *
+     * 
+     * {@code
      * MethodDeclaration "Foo.f(int)"@23/45 in FILE:/tmp/Foo.java
-     * }

+     * }
+     *
*/ String ELEMENT_SHORT = "%c \"%N\" @%p in \"%f\""; } diff --git a/recoder/src/main/java/recoder/java/expression/operator/New.java b/recoder/src/main/java/recoder/java/expression/operator/New.java index fdbb7b02810..a2b2f275a0e 100644 --- a/recoder/src/main/java/recoder/java/expression/operator/New.java +++ b/recoder/src/main/java/recoder/java/expression/operator/New.java @@ -17,8 +17,8 @@ /** * The object allocation operator. There are two variants for New: - *
    - *
  1. Class constructor call
    + *
      + *
    1. Class constructor call
      * * 
        * {@code
@@ -27,15 +27,20 @@
  * }
  *
      * - *
    2. Anonymous Inner Class definition and construction
      + *
      3. + * + *
    3. Anonymous Inner Class definition and construction
      * {@code new XYZ(a_1, ..., a_n)} * * 
      - * {@code{  m_1, ..., m_k
- * if getType() instanceof UserType && getClassDeclaration() != null
+ * {@code
+ *   m_1, ..., m_k
+ *  if getType() instanceof UserType && getClassDeclaration() != null
  * }
  *
      - *
    + * + *
    2. + *
* The access path is null in most cases, except when an inner class constructor is invoked * from an outer instance. */ diff --git a/recoder/src/main/java/recoder/java/reference/EnumConstructorReference.java b/recoder/src/main/java/recoder/java/reference/EnumConstructorReference.java index 30c3d41ed13..46c1643e060 100644 --- a/recoder/src/main/java/recoder/java/reference/EnumConstructorReference.java +++ b/recoder/src/main/java/recoder/java/reference/EnumConstructorReference.java @@ -65,7 +65,7 @@ public StatementContainer getStatementContainer() { /** * @throws UnsupportedOperationException - * @see getStatementContainer() + * @see #getStatementContainer() */ public void setStatementContainer(@SuppressWarnings("unused") StatementContainer c) { throw new UnsupportedOperationException(); diff --git a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java index 89f5265b610..9ccb1b97074 100644 --- a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java @@ -221,10 +221,9 @@ public void modelChanged(ChangeHistoryEvent changes) { } /** - * handles the given change by trying not to invalidate too much pre computed information. + * handles the given change by trying not to invalidate too much pre-computed information. * - * @param attached true if the program elements was attached, false otherwise - * @param changed the program element that was changed + * @param change the change made in the AST */ void processChange(TreeChange change) { // the following code implements a very restrictive way to invalidate @@ -1836,8 +1835,9 @@ public final Constructor getConstructor(ConstructorDeclaration cd) { /** * UNTESTED AND INCOMPLETE * - * @param pe - * @return + * @param m the method to be checked + * @param mr the method reference to be checked + * @return warning/error message or {@code null} if everything was fine */ private final String isAppropriate(Method m, MethodReference mr) { // follows JLS ?15.12.3 From e3880ec46572d6ac0f22ccf91c09d856f34c637c Mon Sep 17 00:00:00 2001 From: unp1 Date: Mon, 30 Oct 2023 14:52:38 +0100 Subject: [PATCH 6/6] Update Format.java --- recoder/src/main/java/recoder/convenience/Format.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/recoder/src/main/java/recoder/convenience/Format.java b/recoder/src/main/java/recoder/convenience/Format.java index a6997e6e1db..ce2338160ec 100644 --- a/recoder/src/main/java/recoder/convenience/Format.java +++ b/recoder/src/main/java/recoder/convenience/Format.java @@ -330,7 +330,7 @@ public static String toString(String formatText, String header, String separator /** * Formats a source element using a default format. - * The default format string is {@code "\"%s\"@%p [%f]"} + * The default format string is {@code "\"%s\"@%p [%f]"} * * @param se the source element to be formatted. * @return a textual representation of the source element.