Document the public API and enforce javadoc doclint

Takes the javadoc doclint warning count from 519 to zero and wires a
doclint check into the build so it stays there.

Twenty of the warnings were defects in existing javadoc: bare @PARAM and
@throws tags with no description, a missing @PARAM on Kind2Api.execute
and Result.setRealPrecision, a missing @return on Util.smtDivide, two
empty <p> tags, and two {@code} blocks nested inside <code> in TypeUtil.
Result.setClosingSymbols also described itself as setting the opening
symbols, and Node.getName documented itself as "the name of the name".

The remaining 499 were undocumented public and protected members across
67 files, now documented: the Kind 2 json labels, the Lustre
pretty-printer visitors, the engine and solver enums, the result value
classes, and the getters and constructors throughout the results
package. Utility classes that only hold statics got private
constructors, which also removes them from the generated docs.

The javadoc task now passes -Xdoclint:all. Gradle always passes -quiet,
which hides warning-level diagnostics and does not fail the build on
them, so a separate doclintCheck task forks javadoc, reads its
diagnostics and fails `check` if any are reported.

Note that JDK 11's javadoc does not report missing comments at all, so
the new check only bites on newer JDKs. The documentation here was
verified against the JDK 25 javadoc, which does report them.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: daniel-larraz

build.gradle

@@ -28,6 +28,63 @@ java {
   withSourcesJar()
 }
 
+tasks.withType(Javadoc).configureEach {
+  options.addBooleanOption('Xdoclint:all', true)
+  failOnError = true
+}
+
+// The javadoc task above runs doclint, but Gradle always passes -quiet, which
+// hides warning-level diagnostics such as "no comment", and it does not fail on
+// them. This task runs doclint separately and fails `check` if anything is
+// reported. Note that JDK 11's javadoc does not report missing comments at all,
+// so this only bites on newer JDKs; the documentation was verified against the
+// JDK 25 javadoc, which does report them.
+def doclintCheck = tasks.register('doclintCheck') {
+  description = 'Runs javadoc doclint over the main sources and fails on any warning.'
+  group = 'verification'
+  dependsOn tasks.named('classes')
+
+  def sources = sourceSets.main.allJava
+  def classpath = sourceSets.main.compileClasspath
+  def workDir = layout.buildDirectory.dir('tmp/doclint')
+
+  inputs.files(sources)
+  inputs.files(classpath)
+  outputs.dir(workDir)
+
+  doLast {
+    def dir = workDir.get().asFile
+    dir.deleteDir()
+    dir.mkdirs()
+
+    // The in-process javadoc ToolProvider does not honour -Xdoclint, so fork the
+    // real javadoc executable and read its diagnostics.
+    def argFile = new File(dir, 'sources.txt')
+    argFile.text = sources.files.collect { it.absolutePath }.join('\n')
+
+    def command = ["${System.getProperty('java.home')}/bin/javadoc".toString(),
+                   '-Xdoclint:all', '-Xmaxwarns', '100000',
+                   '-classpath', classpath.asPath,
+                   '-d', new File(dir, 'out').absolutePath,
+                   '@' + argFile.absolutePath]
+
+    def process = new ProcessBuilder(command).redirectErrorStream(true).start()
+    def output = process.inputStream.text
+    def exitCode = process.waitFor()
+
+    def problems = output.readLines().findAll { it =~ /: (warning|error): / }
+    if (exitCode != 0 || !problems.isEmpty()) {
+      problems.each { logger.error(it) }
+      throw new GradleException(
+          "javadoc doclint reported ${problems.size()} problem(s); see the messages above.")
+    }
+  }
+}
+
+tasks.named('check') {
+  dependsOn doclintCheck
+}
+
 publishing {
   publications {
     maven(MavenPublication) {

src/main/java/StopWatch.java

@@ -25,6 +25,9 @@
  * Program.
  */
 public class StopWatch {
+  private StopWatch() {
+  }
+
   /**
    * Run the main function to print the generated Lustre program and results of calling Kind 2.
    *

src/main/java/edu/uiowa/cs/clc/kind2/Assert.java

@@ -8,19 +8,43 @@
 
 package edu.uiowa.cs.clc.kind2;
 
+/**
+ * Simple runtime assertions used to validate arguments.
+ */
 public class Assert {
+  private Assert() {
+  }
+
+  /**
+   * Asserts that the given object is not null.
+   *
+   * @param o the object to check
+   * @throws IllegalArgumentException if {@code o} is null
+   */
   public static void isNotNull(Object o) {
     if (o == null) {
       throw new Kind2Exception("Object unexpectedly null");
     }
   }
 
+  /**
+   * Asserts that the given condition holds.
+   *
+   * @param b the condition to check
+   * @throws IllegalArgumentException if {@code b} is false
+   */
   public static void isTrue(boolean b) {
     if (!b) {
       throw new Kind2Exception("Assertion failed");
     }
   }
 
+  /**
+   * Asserts that the given condition does not hold.
+   *
+   * @param b the condition to check
+   * @throws IllegalArgumentException if {@code b} is true
+   */
   public static void isFalse(boolean b) {
     if (b) {
       throw new Kind2Exception("Assertion failed");

src/main/java/edu/uiowa/cs/clc/kind2/Kind2Exception.java

@@ -14,10 +14,21 @@
 public class Kind2Exception extends RuntimeException {
   private static final long serialVersionUID = 1L;
 
+  /**
+   * Constructs an exception with the given message.
+   *
+   * @param message the detail message
+   */
   public Kind2Exception(String message) {
     super(message);
   }
 
+  /**
+   * Constructs an exception with the given message and cause.
+   *
+   * @param message the detail message
+   * @param t the underlying cause
+   */
   public Kind2Exception(String message, Throwable t) {
     super(message, t);
   }

src/main/java/edu/uiowa/cs/clc/kind2/api/ApiUtil.java

@@ -18,15 +18,41 @@
 import edu.uiowa.cs.clc.kind2.Kind2Exception;
 import edu.uiowa.cs.clc.kind2.util.Util;
 
+/**
+ * Helpers for writing Kind 2 input files and reading its output.
+ */
 public class ApiUtil {
+  private ApiUtil() {
+  }
+
+  /**
+   * Writes a Lustre program to a temporary file for Kind 2 to read.
+   *
+   * @param program the Lustre program text
+   * @return the file the program was written to
+   */
   public static File writeLustreFile(String program) {
     return writeTempFile("kind2-api-", ".lus", program);
   }
 
+  /**
+   * Writes an interpreter input to a temporary file for Kind 2 to read.
+   *
+   * @param program the interpreter input text
+   * @return the file the input was written to
+   */
   public static File writeInterpreterFile(String program) {
     return writeTempFile("kind2-api-", ".json", program);
   }
 
+  /**
+   * Writes the given contents to a new temporary file.
+   *
+   * @param fileName the base name of the file
+   * @param fileExt the file extension, may be null
+   * @param contents the text to write, may be null to leave the file empty
+   * @return the newly created file
+   */
   public static File writeTempFile(String fileName, String fileExt, String contents) {
     File file = null;
     try {
@@ -40,6 +66,13 @@ public static File writeTempFile(String fileName, String fileExt, String content
     }
   }
 
+  /**
+   * Reads a stream to its end.
+   *
+   * @param inputStream the stream to read
+   * @return the full contents of the stream
+   * @throws java.io.IOException if the stream cannot be read
+   */
   public static String readAll(InputStream inputStream) throws IOException {
     StringBuilder result = new StringBuilder();
     BufferedInputStream buffered = new BufferedInputStream(inputStream);
@@ -50,6 +83,12 @@ public static String readAll(InputStream inputStream) throws IOException {
     return result.toString();
   }
 
+  /**
+   * Renders a command line with each argument quoted.
+   *
+   * @param pieces the command and its arguments
+   * @return the quoted command line
+   */
   public static String getQuotedCommand(List<String> pieces) {
     return pieces.stream().map(p -> p.contains(" ") ? "\"" + p + "\"" : p).collect(joining(" "));
   }

src/main/java/edu/uiowa/cs/clc/kind2/api/DebugLogger.java

@@ -15,13 +15,27 @@
 import edu.uiowa.cs.clc.kind2.Kind2Exception;
 import edu.uiowa.cs.clc.kind2.util.Util;
 
+/**
+ * Writes Kind 2 debug output to a temporary file.
+ * <p>
+ * A logger built with the no-argument constructor discards everything written to it.
+ */
 public class DebugLogger {
   private final PrintWriter debug;
 
+  /**
+   * Constructs a logger that discards all output.
+   */
   public DebugLogger() {
     debug = null;
   }
 
+  /**
+   * Constructs a logger writing to a new temporary file.
+   *
+   * @param prefix the prefix of the temporary file's name
+   * @throws edu.uiowa.cs.clc.kind2.Kind2Exception if the file cannot be created
+   */
   public DebugLogger(String prefix) {
     try {
       File debugFile = File.createTempFile(prefix, ".txt");
@@ -31,18 +45,32 @@ public DebugLogger(String prefix) {
     }
   }
 
+  /**
+   * Writes an empty line.
+   */
   public void println() {
     if (debug != null) {
       debug.println();
     }
   }
 
+  /**
+   * Writes a line of text.
+   *
+   * @param text the text to write
+   */
   public void println(String text) {
     if (debug != null) {
       debug.println(text);
     }
   }
 
+  /**
+   * Writes a line of text followed by the contents of a file.
+   *
+   * @param text the text to write
+   * @param file the file whose contents to append
+   */
   public void println(String text, File file) {
     if (debug != null) {
       try {
@@ -53,6 +81,14 @@ public void println(String text, File file) {
     }
   }
 
+  /**
+   * Saves the given contents to a temporary file for later inspection.
+   *
+   * @param prefix the prefix of the file's name
+   * @param suffix the suffix of the file's name
+   * @param contents the text to write
+   * @return the file written, or null if debugging is off
+   */
   public File saveFile(String prefix, String suffix, String contents) {
     if (debug != null) {
       try {
@@ -67,6 +103,11 @@ public File saveFile(String prefix, String suffix, String contents) {
     }
   }
 
+  /**
+   * Deletes a file unless debugging is enabled, in which case it is kept.
+   *
+   * @param file the file to delete
+   */
   public void deleteIfUnneeded(File file) {
     if (debug == null && file != null && file.exists()) {
       file.delete();

src/main/java/edu/uiowa/cs/clc/kind2/api/ITPSolverOption.java

@@ -7,8 +7,30 @@
 
 package edu.uiowa.cs.clc.kind2.api;
 
+/**
+ * The solvers Kind 2 can use to compute interpolants.
+ */
 public enum ITPSolverOption {
-  CVC5QE, MATHSAT, OPENSMT, SMTINTERPOL, Z3QE;
+  /**
+   * The cvc5 solver using quantifier elimination.
+   */
+  CVC5QE,
+  /**
+   * The MathSAT solver.
+   */
+  MATHSAT,
+  /**
+   * The OpenSMT solver.
+   */
+  OPENSMT,
+  /**
+   * The SMTInterpol solver.
+   */
+  SMTINTERPOL,
+  /**
+   * The Z3 solver using quantifier elimination.
+   */
+  Z3QE;
 
   @Override
   public String toString() {

src/main/java/edu/uiowa/cs/clc/kind2/api/IVCCategory.java

@@ -7,8 +7,30 @@
 
 package edu.uiowa.cs.clc.kind2.api;
 
+/**
+ * The categories of model elements that may appear in an inductive validity core.
+ */
 public enum IVCCategory {
-  NODECALLS, CONTRACTS, EQUATIONS, ASSERTIONS, ANNOTATIONS;
+  /**
+   * Calls to other components.
+   */
+  NODECALLS,
+  /**
+   * Contract items such as assumptions and guarantees.
+   */
+  CONTRACTS,
+  /**
+   * Equations defining variables.
+   */
+  EQUATIONS,
+  /**
+   * Assertions stated in the component.
+   */
+  ASSERTIONS,
+  /**
+   * Annotations such as the main annotation.
+   */
+  ANNOTATIONS;
 
   @Override
   public String toString() {