From 981dedd6d2c511b136b2e09b57662ff82ceb9f52 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 21 Aug 2026 01:24:55 +0200 Subject: [PATCH 01/11] Add support for generation of varcond and proof script documentation --- build.gradle | 4 +- gradle/libs.versions.toml | 6 + key.core/build.gradle | 5 +- .../java/de/uka/ilkd/key/doc/ScriptDoc.java | 27 ++ .../java/de/uka/ilkd/key/doc/VarcondDoc.java | 107 +++++++ .../key/nparser/builder/TacletPBuilder.java | 2 +- .../varexp/AbstractConditionBuilder.java | 12 +- .../varexp/AbstractTacletBuilderCommand.java | 29 +- .../ilkd/key/nparser/varexp/ArgumentType.java | 9 +- .../varexp/ConstructorBasedBuilder.java | 28 +- .../nparser/varexp/TacletBuilderCommand.java | 7 +- .../varexp/TacletBuilderCommandInfo.java | 291 ++++++++++++++++++ .../varexp/TacletBuilderManipulators.java | 58 ++-- .../ilkd/key/nparser/varexp/package-info.java | 9 + .../key/scripts/meta/ArgumentsLifter.java | 74 ++--- 15 files changed, 550 insertions(+), 118 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java diff --git a/build.gradle b/build.gradle index 93b792ef77c..5d3edfa1a90 100644 --- a/build.gradle +++ b/build.gradle @@ -84,6 +84,9 @@ subprojects { testImplementation(libs.logback.classic) + // Therapi runtime javadoc + annotationProcessor 'com.github.therapi:therapi-runtime-javadoc-scribe:0.13.0' + implementation 'com.github.therapi:therapi-runtime-javadoc:0.13.0' compileOnly(libs.jspecify) testCompileOnly(libs.jspecify) compileOnly(libs.checkerframework.qual) @@ -316,7 +319,6 @@ subprojects { afterEvaluate { description = project.description assert (project.description != null && project.description != "") : "Description of modules are required at maven-central" - print(project.description) } url = 'https://key-project.org/' diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 7ddff7e2730..8038c479dfe 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -25,6 +25,7 @@ stringtemplate = "4.3.4" javapoet = "1.13.0" javaparser = "3.28.0-K13.6" truth = "1.4.5" +therapi = "0.13.0" # UI and CLI flatlaf = "3.7.2" @@ -35,6 +36,7 @@ docking-frames = "1.1.3p1" # External tools scala-isabelle = "0.4.5" + [libraries] # SLF4J and logging slf4j-api = { module = "org.slf4j:slf4j-api", version.ref = "slf4j" } @@ -43,6 +45,10 @@ logback-classic = { module = "ch.qos.logback:logback-classic", version.ref = "lo # JSpecify (nullability annotations) jspecify = { module = "org.jspecify:jspecify", version.ref = "jspecify" } +#Extracting Javadoc +therapi-processor = { module = "com.github.therapi:therapi-runtime-javadoc-scribe", version.ref = "therapi" } +therapi-runtime = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" } + # EISOP Checker Framework checkerframework-qual = { module = "io.github.eisop:checker-qual", version.ref = "eisop" } checkerframework-util = { module = "io.github.eisop:checker-util", version.ref = "eisop" } diff --git a/key.core/build.gradle b/key.core/build.gradle index c6584ca35ab..7567393c7fb 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -24,6 +24,9 @@ dependencies { testImplementation(libs.truth) testImplementation(project(":key.core")) + annotationProcessor(libs.therapi.processor) + api(libs.therapi.runtime) + // https://mvnrepository.com/artifact/com.fasterxml.jackson.dataformat/jackson-dataformat-yaml testImplementation(libs.jackson.dataformat.yaml) @@ -32,7 +35,7 @@ dependencies { } tasks.withType(JavaCompile).configureEach { - options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts" + options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts,de.uka.ilkd.key.rule.conditions" } // The target directory for JavaCC (parser generation) diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java new file mode 100644 index 00000000000..ae9d19210a5 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java @@ -0,0 +1,27 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.doc; + +import java.util.ArrayList; +import java.util.Comparator; + +import de.uka.ilkd.key.scripts.ProofScriptCommand; +import de.uka.ilkd.key.scripts.ProofScriptEngine; + +/** + * + * @author Alexander Weigl + * @version 1 (23.08.26) + */ +public class ScriptDoc { + public static void main(String[] args) { + var commands = new ArrayList<>(ProofScriptEngine.loadCommands().values()); + commands.sort(Comparator.comparing(ProofScriptCommand::getName)); + + for (var command : commands) { + System.out.println(command.getDocumentation()); + System.out.println("\n\n\n"); + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java new file mode 100644 index 00000000000..08403ae95a2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java @@ -0,0 +1,107 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.doc; + +import java.util.Arrays; +import java.util.Comparator; +import java.util.function.Function; +import java.util.stream.Collectors; + +import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommand; +import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommandInfo; +import de.uka.ilkd.key.nparser.varexp.TacletBuilderManipulators; + +import com.github.javaparser.ParserConfiguration; +import com.github.javaparser.StaticJavaParser; +import com.github.therapi.runtimejavadoc.CommentFormatter; +import com.google.common.collect.Streams; +import org.jspecify.annotations.Nullable; + +/** + * + * @author Alexander Weigl + * @version 1 (23.08.26) + */ +public class VarcondDoc { + // region + public static void main(String[] args) { + var config = new ParserConfiguration(); + config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_21); + StaticJavaParser.setConfiguration(config); + + Function normalizeCmdName = + (String it) -> it.startsWith("\\") ? it.replace("\\\\", "\\") : "\\" + it; + Function getTriggerName = TacletBuilderCommandInfo::name; + + var g = TacletBuilderManipulators.getConditionBuilders().stream() + .map(TacletBuilderCommand::getInformation) + .collect(Collectors.groupingBy(getTriggerName.andThen(normalizeCmdName))); + Comparator reversed = + Comparator.comparing((TacletBuilderCommandInfo it) -> it.argumentTypes().length) + .reversed(); + + var conds = g.keySet().stream().sorted().toList(); + + for (var name : conds) { + var cmds = g.get(name); + System.out.println(); + System.out.println(); + System.out.format("### `%s`\n\n", name); + cmds.sort(reversed); + + final var generalDocumentation = cmds.getFirst().getGeneralDocumentation(); + System.out.println( + cleanJavadoc(new CommentFormatter().format(generalDocumentation.getComment()))); + + System.out.format("\n**Signatures**\n\n"); + for (TacletBuilderCommandInfo cmd : cmds) { + + final var arguments = Streams.zip( + Arrays.stream(cmd.argNames()), + Arrays.stream(cmd.argumentTypes()).map(Enum::toString), + "%s: %s"::formatted) + .collect(Collectors.joining(", ")); + System.out.printf("* `%s(%s)`\n", name, arguments); + + if (cmd.isNegationSupported()) { + System.out.printf("* `\\not%s(%s)`\n", name, arguments); + } + + System.out.println(); + final var argumentInformation = cmd.getArgumentInformation(); + + System.out.println( + indent(" ", cleanJavadoc(argumentInformation.getComment().toString()))); + System.out.println(); + argumentInformation.getParams().stream() + .map(tag -> " * `%s` %s".formatted(tag.getName(), tag.getComment())) + .forEach(System.out::println); + System.out.println(); + } + } + } + + private static String indent(String spaces, String it) { + return spaces + it.replace("\n", "\n" + spaces); + } + + private static String cleanJavadoc(@Nullable String it) { + if (it == null) + it = ""; + return it.replace("", "`") + .replace("
    ", "\n") + .replace("
", "\n") + .replace("
    ", "\n") + .replace("
  • ", "* ") + .replace("
    • ", "") + .replace("{@link", "`") + .replace("}", "`") + .replace("", "`") + .replace("    ", "`") + .replace("", "`") + .replace("", "**") + .replace("", "**"); + } + // endregion +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 9d0979d5650..3aca30f2b35 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -801,7 +801,7 @@ public Object visitVarexp(JavaKeYParser.VarexpContext ctx) { } if (!applied) { LOGGER.warn("Found name-matching conditions with following type signature:"); - suitableManipulators.forEach(it -> LOGGER.warn(Arrays.toString(it.getArgumentTypes()))); + suitableManipulators.forEach(it -> LOGGER.warn(it.getArgumentTypes().toString())); LOGGER.warn("But you gave {} arguments.\n", arguments.size()); semanticError(ctx, "Could not apply the given variable condition: %s", ctx.getText()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java index 87d292ddc0b..bf371d002e6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java @@ -4,7 +4,7 @@ * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.nparser.varexp; -import org.jspecify.annotations.NonNull; +import org.key_project.prover.rules.VariableCondition; /** * @author Alexander Weigl @@ -12,8 +12,12 @@ */ public abstract class AbstractConditionBuilder extends AbstractTacletBuilderCommand implements ConditionBuilder { - protected AbstractConditionBuilder(@NonNull String triggerName, - @NonNull ArgumentType... argumentsTypes) { - super(triggerName, argumentsTypes); + protected AbstractConditionBuilder(TacletBuilderCommandInfo info) { + super(info); + } + + public AbstractConditionBuilder(String name, Class clazz, + boolean negationSupported, ArgumentType... types) { + super(TacletBuilderCommandInfo.createVarcondInfo(name, clazz, negationSupported, types)); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java index 9c0783554c8..79090c9f933 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java @@ -4,7 +4,6 @@ * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.nparser.varexp; -import org.jspecify.annotations.NonNull; /** * Simple default implementation for {@link TacletBuilderCommand}. @@ -13,36 +12,26 @@ * @version 1 (12/9/19) */ public abstract class AbstractTacletBuilderCommand implements TacletBuilderCommand { - private final @NonNull String triggerName; - private final @NonNull ArgumentType[] argumentsTypes; + protected final TacletBuilderCommandInfo info; - /** - * Construct this class with the parameters for {@link #isSuitableFor(String)} and - * {@link #getArgumentTypes()}. - * - * @param triggerName the name of this command. - * @param argumentsTypes the argument type of this command. - */ - protected AbstractTacletBuilderCommand(@NonNull String triggerName, - @NonNull ArgumentType... argumentsTypes) { - this.triggerName = triggerName; - this.argumentsTypes = argumentsTypes; + protected AbstractTacletBuilderCommand(TacletBuilderCommandInfo info) { + this.info = info; } @Override - public boolean isSuitableFor(@NonNull String name) { - if (triggerName.equalsIgnoreCase(name)) { + public boolean isSuitableFor(String name) { + if (info.name().equalsIgnoreCase(name)) { return true; } - if (name.startsWith("\\")) // handling leading backslashes - { + // handling leading backslashes + if (name.startsWith("\\")) { return isSuitableFor(name.substring(1)); } return false; } @Override - public ArgumentType[] getArgumentTypes() { - return argumentsTypes; + public TacletBuilderCommandInfo getInformation() { + return info; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java index 0a20eb11606..e681c95db69 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java @@ -13,14 +13,19 @@ /** * Argument types for {@link TacletBuilderCommand}s. + * Each {@link ArgumentType} has an expected class for the type of the argument. * * @author Alexander Weigl * @version 1 (12/9/19) * @see TacletBuilderCommand */ public enum ArgumentType { - TYPE_RESOLVER(TypeResolver.class), SORT(Sort.class), TERM(JTerm.class), - JAVA_TYPE(KeYJavaType.class), VARIABLE(ParsableVariable.class), STRING(String.class); + TYPE_RESOLVER(TypeResolver.class), + SORT(Sort.class), + TERM(JTerm.class), + JAVA_TYPE(KeYJavaType.class), + VARIABLE(ParsableVariable.class), + STRING(String.class); public final Class clazz; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java index 96872e61a4d..3e248f6fcda 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java @@ -13,39 +13,26 @@ public class ConstructorBasedBuilder extends AbstractConditionBuilder { private final Class clazz; - private final boolean negationSupported; public ConstructorBasedBuilder(String name, Class clazz, ArgumentType... types) { - this(name, lastArgumentOfFirstContructorIsBoolean(clazz), clazz, types); + this(TacletBuilderCommandInfo.createVarcondInfo(name, clazz, types), clazz); } - private static boolean lastArgumentOfFirstContructorIsBoolean( + public ConstructorBasedBuilder(TacletBuilderCommandInfo info, Class clazz) { - try { - Class[] types = clazz.getConstructors()[0].getParameterTypes(); - return types[types.length - 1] == Boolean.class - || types[types.length - 1] == Boolean.TYPE; - } catch (ArrayIndexOutOfBoundsException e) { - return false; - } - } - - public ConstructorBasedBuilder(String name, boolean negationSupported, - Class clazz, ArgumentType... types) { - super(name, types); + super(info); this.clazz = clazz; - this.negationSupported = negationSupported; } @Override public VariableCondition build(Object[] arguments, List parameters, boolean negated) { - if (negated && !negationSupported) { + if (negated && !info.isNegationSupported()) { throw new RuntimeException(clazz.getName() + " does not support negation."); } Object[] args = arguments; - if (negationSupported) { + if (info.isNegationSupported()) { args = Arrays.copyOf(arguments, arguments.length + 1); args[args.length - 1] = negated; } @@ -59,4 +46,9 @@ public VariableCondition build(Object[] arguments, List parameters, bool } throw new RuntimeException(); } + + @Override + public TacletBuilderCommandInfoImpl getInformation() { + return (TacletBuilderCommandInfoImpl) super.getInformation(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java index a72227f8035..e6b7f3e6675 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java @@ -28,6 +28,9 @@ public interface TacletBuilderCommand { */ boolean isSuitableFor(@NonNull String name); + /// Returns information about this command. + TacletBuilderCommandInfo getInformation(); + /** * Defines the amount and type of expected arguments. For example, if you want describe a * sub-type test (instanceOf) you would need two sorts {@code new ArgumentType[]{SORT,SORT} } as @@ -39,7 +42,9 @@ public interface TacletBuilderCommand { * * @see ArgumentType */ - ArgumentType[] getArgumentTypes(); + default ArgumentType[] getArgumentTypes() { + return getInformation().argumentTypes(); + } /** * Applying this command on the given taclet builder. diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java new file mode 100644 index 00000000000..225fb5a1247 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java @@ -0,0 +1,291 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.nparser.varexp; + +import java.lang.reflect.Constructor; +import java.util.Arrays; +import java.util.List; + +import com.github.therapi.runtimejavadoc.ClassJavadoc; +import com.github.therapi.runtimejavadoc.MethodJavadoc; +import com.github.therapi.runtimejavadoc.ParamJavadoc; +import com.github.therapi.runtimejavadoc.RuntimeJavadoc; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +/// Describes a single "variable condition" (varcond) or taclet-builder command that can be +/// used inside taclet definitions, together with metadata needed to parse, validate, and +/// document its usage. +/// +/// An instance of this interface bundles together: +/// +/// - the command's [`name`][#name()] as it appears in taclet source files, +/// - the expected [`argument types`][#argumentTypes()], +/// - whether the command [`supports negation`][#isNegationSupported()] (i.e. an +/// additional trailing `boolean` constructor argument), +/// - and Javadoc-derived documentation for both the command itself and its individual +/// arguments, extracted via reflection from the backing implementation class. +/// +/// Instances are typically created via the [#createVarcondInfo] factory methods rather +/// than by implementing this interface directly. +/// +/// @author Alexander Weigl +/// @version 1 (23.08.26) +@NullMarked +public interface TacletBuilderCommandInfo { + + /// Returns the name of this command as used in taclet source files. + /// + /// @return the command name, never `null` + String name(); + + /// Returns the declared types of the arguments accepted by this command, in the order + /// they must appear in the taclet source. + /// + /// @return the array of argument types + ArgumentType[] argumentTypes(); + + /// Returns the names of the arguments as declared in the backing implementation's + /// constructor (or as documented via Javadoc, if available). + /// + /// Resolving the argument names requires reflecting on the implementation class and is + /// performed lazily on first access. + /// + /// @return the array of argument names, in the same order as [#argumentTypes()] + String[] argNames(); + + /// Indicates whether this command supports an optional trailing negation flag, i.e. + /// whether the backing implementation class has a constructor whose parameters are the + /// declared [`argument types`][#argumentTypes()] followed by an additional + /// `boolean` parameter. + /// + /// @return `true` if negation is supported, `false` otherwise + boolean isNegationSupported(); + + /// Returns the class-level Javadoc documentation extracted from the backing + /// implementation class. This is typically used as the general description of what the + /// command does. + /// + /// @return the class-level Javadoc, never `null` + ClassJavadoc getGeneralDocumentation(); + + /// Returns the Javadoc documentation of the specific constructor that matches this + /// command's argument types (and negation flag, if supported). This is typically used + /// to document the individual arguments of the command. + /// + /// @return the matching constructor's Javadoc, or a documentation object with empty + /// fields if no Javadoc could be resolved + MethodJavadoc getArgumentInformation(); + + /// Creates a [TacletBuilderCommandInfo] for a command whose negation support is + /// determined automatically by inspecting the constructors of `clazz`. + /// + /// @param name the name of the command as used in taclet source files + /// @param clazz the implementation class backing this command + /// @param types the expected argument types, in declaration order + /// @return a new [TacletBuilderCommandInfo] instance + static TacletBuilderCommandInfo createVarcondInfo(String name, Class clazz, + ArgumentType... types) { + return new TacletBuilderCommandInfoImpl(name, types, clazz, null); + } + + /// Creates a [TacletBuilderCommandInfo] for a command with an explicitly specified + /// negation support flag, instead of determining it via reflection. + /// + /// @param name the name of the command as used in taclet source files + /// @param clazz the implementation class backing this command + /// @param negationSupported whether the command supports a trailing negation argument + /// @param types the expected argument types, in declaration order + /// @return a new [TacletBuilderCommandInfo] instance + static TacletBuilderCommandInfo createVarcondInfo(String name, Class clazz, + Boolean negationSupported, ArgumentType... types) { + return new TacletBuilderCommandInfoImpl(name, types, clazz, negationSupported); + } +} + + +/// Default implementation of [TacletBuilderCommandInfo]. +/// +/// Argument names and documentation are resolved lazily, on first access, by reflecting on +/// the backing implementation class ([#clazz]) and looking up its runtime Javadoc via +/// [RuntimeJavadoc]. +class TacletBuilderCommandInfoImpl implements TacletBuilderCommandInfo { + /// The name of the command as used in taclet source files. + public final String name; + /// The expected argument types, in declaration order. + private final ArgumentType[] argTypes; + /// The implementation class backing this command, used for reflection-based lookups. + private final Class clazz; + /// Whether this command supports a trailing negation argument. `null` until + /// lazily resolved via [#isNegationSupported()]. + private @Nullable Boolean isNegationSupported; + /// The resolved argument names, or `null` until [#findDocumentation()] has run. + private String @Nullable [] argNames; + /// The resolved class-level Javadoc, or `null` until [#findDocumentation()] has run. + private @Nullable ClassJavadoc generalDocumentation; + /// The resolved constructor Javadoc, or `null` until [#findDocumentation()] has run. + private @Nullable MethodJavadoc argumentDocumentation; + + /// Creates a new command descriptor. + /// + /// @param name the name of the command as used in taclet source files + /// @param types the expected argument types, in declaration order + /// @param clazz the implementation class backing this command + /// @param negationSupported whether the command supports a trailing negation argument, + /// or `null` to determine this lazily via reflection + public TacletBuilderCommandInfoImpl(String name, ArgumentType[] types, Class clazz, + @Nullable Boolean negationSupported) { + this.name = name; + argTypes = types; + this.clazz = clazz; + isNegationSupported = negationSupported; + } + + @Override + public String name() { + return name; + } + + @Override + public ArgumentType[] argumentTypes() { + return argTypes; + } + + @Override + public String[] argNames() { + if (argNames == null) { + findDocumentation(); + } + return argNames; + } + + @Override + public boolean isNegationSupported() { + if (isNegationSupported == null) { + isNegationSupported = lastArgumentOfFirstConstructorIsBoolean(clazz, argTypes); + } + return isNegationSupported; + } + + @Override + public ClassJavadoc getGeneralDocumentation() { + if (generalDocumentation == null) { + findDocumentation(); + } + return generalDocumentation; + } + + @Override + public MethodJavadoc getArgumentInformation() { + if (argumentDocumentation == null) { + findDocumentation(); + } + return argumentDocumentation; + } + + /// Computes the parameter types of the constructor that this command's arguments (and, + /// if applicable, its negation flag) would map to. + /// + /// @return the array of expected constructor parameter types + Class[] getConstructorClasses() { + return getConstructorClasses(argTypes, isNegationSupported()); + } + + /// Resolves and caches [#argNames], [#generalDocumentation], and + /// [#argumentDocumentation] by reflecting on [#clazz] and looking up its + /// matching constructor's runtime Javadoc. + /// + /// If no constructor matching [#getConstructorClasses()] can be found, argument + /// names are filled with empty strings and empty documentation placeholders are used + /// instead of failing. + private void findDocumentation() { + ClassJavadoc classDoc = RuntimeJavadoc.getJavadoc(clazz.getName()); + generalDocumentation = classDoc; + + final var constr = findConstructor(clazz, getConstructorClasses()); + if (constr == null) { + argNames = new String[argTypes.length]; + Arrays.fill(argNames, ""); + argumentDocumentation = + MethodJavadoc.createEmpty((Constructor) null); + return; + } + + final var constructorDeclaration = classDoc.getConstructors() + .stream().filter(it -> it.matches(constr)).findAny(); + + final var parameters = constr.getParameters(); + argNames = new String[argTypes.length]; + for (int i = 0; i < argTypes.length; i++) { + argNames[i] = parameters[i].getName(); + } + + constructorDeclaration.ifPresent(it -> { + List params = it.getParams(); + for (int i = 0; i < argNames.length; i++) { + argNames[i] = params.get(i).getName(); + } + }); + + argumentDocumentation = constructorDeclaration + .orElse(MethodJavadoc.createEmpty((Constructor) null)); + // endregion + } + + + /// Checks whether `clazz` declares a constructor whose parameter types are + /// `argTypes` followed by a trailing `boolean` parameter, which indicates + /// support for an optional negation flag. + /// + /// @param clazz the implementation class to inspect + /// @param argTypes the expected leading argument types + /// @return `true` if such a constructor exists, `false` otherwise + /// @throws IllegalStateException if no suitable constructor exists in `clazz` + private static boolean lastArgumentOfFirstConstructorIsBoolean( + Class clazz, ArgumentType[] argTypes) { + if (findConstructor(clazz, getConstructorClasses(argTypes, true)) != null) { + return true; + } + if (findConstructor(clazz, getConstructorClasses(argTypes, false)) != null) { + return false; + } + throw new IllegalStateException(); + } + + private static @Nullable Constructor findConstructor(Class clazz, + Class[] constructorClasses) { + final var constructors = clazz.getConstructors(); + c: for (var constructor : constructors) { + if (constructor.getParameterCount() != constructorClasses.length) + continue; + final var parameterTypes = constructor.getParameterTypes(); + for (var i = 0; i < parameterTypes.length; i++) { + if (!constructorClasses[i].isAssignableFrom(parameterTypes[i])) { + continue c; + } + } + return constructor; + } + return null; + } + + /// Builds the array of constructor parameter types corresponding to `argTypes`, + /// optionally appending `boolean.class` for negation support. + /// + /// @param argTypes the declared argument types + /// @param isNegationSupported whether a trailing `boolean` parameter should be + /// appended for negation support + /// @return the resulting array of constructor parameter types + static Class[] getConstructorClasses(ArgumentType[] argTypes, boolean isNegationSupported) { + Class[] clazzes = new Class[argTypes.length + (isNegationSupported ? 1 : 0)]; + for (int i = 0; i < argTypes.length; i++) { + clazzes[i] = argTypes[i].clazz; + } + + if (isNegationSupported) + clazzes[clazzes.length - 1] = Boolean.TYPE; + return clazzes; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 99c439548ff..c3c5691835b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -15,17 +15,19 @@ import de.uka.ilkd.key.logic.op.JOperatorSV; import de.uka.ilkd.key.logic.op.ProgramSV; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.rule.NewVarcond; import de.uka.ilkd.key.rule.conditions.*; import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.VariableCondition; - -import org.jspecify.annotations.NonNull; +import org.key_project.prover.rules.conditions.NewDependingOn; +import org.key_project.prover.rules.conditions.NotFreeIn; import static de.uka.ilkd.key.nparser.varexp.ArgumentType.SORT; import static de.uka.ilkd.key.nparser.varexp.ArgumentType.TYPE_RESOLVER; +import static de.uka.ilkd.key.nparser.varexp.TacletBuilderCommandInfo.createVarcondInfo; import static de.uka.ilkd.key.rule.conditions.TypeComparisonCondition.Mode.*; /** @@ -37,6 +39,7 @@ */ public class TacletBuilderManipulators { // region Factories + // Short cut for argument types private static final ArgumentType TR = TYPE_RESOLVER; private static final ArgumentType KJT = ArgumentType.JAVA_TYPE; @@ -51,20 +54,14 @@ public class TacletBuilderManipulators { private static final ArgumentType T = ArgumentType.TERM; - /** - * - */ public static final AbstractConditionBuilder ABSTRACT_OR_INTERFACE = new ConstructorBasedBuilder("isAbstractOrInterface", AbstractOrInterfaceType.class, TR); public static final AbstractConditionBuilder FINAL_TYPE = new ConstructorBasedBuilder("isFinal", FinalTypeVarCond.class, TR); - /** - * - */ public static final AbstractConditionBuilder SAME = - new AbstractConditionBuilder("same", TR, TR) { + new AbstractConditionBuilder("same", TypeComparisonCondition.class, true, TR, TR) { @Override public TypeComparisonCondition build(Object[] arguments, List parameters, boolean negated) { @@ -74,11 +71,8 @@ public TypeComparisonCondition build(Object[] arguments, List parameters } }; - /** - * - */ public static final AbstractConditionBuilder IS_SUBTYPE = - new AbstractConditionBuilder("sub", TR, TR) { + new AbstractConditionBuilder("sub", TypeComparisonCondition.class, true, TR, TR) { @Override public TypeComparisonCondition build(Object[] arguments, List parameters, boolean negated) { @@ -92,9 +86,9 @@ public TypeComparisonCondition build(Object[] arguments, List parameters * */ public static final AbstractConditionBuilder STRICT = - new AbstractConditionBuilder("scrictSub", TR, TR) { + new AbstractConditionBuilder("scrictSub", TypeComparisonCondition.class, false, TR, TR) { @Override - public boolean isSuitableFor(@NonNull String name) { + public boolean isSuitableFor(String name) { if (super.isSuitableFor(name)) { return true; } @@ -117,7 +111,8 @@ public TypeComparisonCondition build(Object[] arguments, List parameters * */ public static final AbstractConditionBuilder DISJOINT_MODULO_NULL = - new AbstractConditionBuilder("disjointModuloNull", TR, TR) { + new AbstractConditionBuilder("disjointModuloNull", TypeComparisonCondition.class, false, TR, + TR) { @Override public TypeComparisonCondition build(Object[] arguments, List parameters, boolean negated) { @@ -139,7 +134,8 @@ public TypeComparisonCondition build(Object[] arguments, List parameters * */ public static final AbstractTacletBuilderCommand NEW_JAVATYPE = - new AbstractTacletBuilderCommand("new", SV, KJT) { + new AbstractTacletBuilderCommand( + createVarcondInfo("new", NewVarcond.class, false, SV, KJT)) { @Override public void apply(TacletBuilder tacletBuilder, Object[] arguments, List parameters, boolean negated) { @@ -152,7 +148,8 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, }; public static final AbstractTacletBuilderCommand NEW_VAR = - new AbstractTacletBuilderCommand("new", SV, SORT) { + new AbstractTacletBuilderCommand( + createVarcondInfo("new", NewVarcond.class, false, SV, SORT)) { @Override public void apply(TacletBuilder tacletBuilder, Object[] arguments, List parameters, boolean negated) { @@ -169,8 +166,8 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, "newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV); static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand { - public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) { - super("notFreeIn", argumentsTypes); + public NotFreeInTacletBuilderCommand(ArgumentType... argumentsTypes) { + super(createVarcondInfo("notFreeIn", NotFreeIn.class, true, argumentsTypes)); } @Override @@ -196,7 +193,8 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, private static final List tacletBuilderCommands = new ArrayList<>(32); public static final AbstractTacletBuilderCommand NEW_TYPE_OF = - new AbstractTacletBuilderCommand("newTypeOf", SV, SV) { + new AbstractTacletBuilderCommand( + createVarcondInfo("newTypeOf", NewVarcond.class, false, SV, SV)) { @Override public void apply(TacletBuilder tacletBuilder, Object[] arguments, @@ -210,7 +208,8 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, } }; public static final AbstractTacletBuilderCommand NEW_DEPENDING_ON = - new AbstractTacletBuilderCommand("newDependingOn", SV, SV) { + new AbstractTacletBuilderCommand( + createVarcondInfo("newDependingOn", NewDependingOn.class, false, SV, SV)) { @Override public void apply(TacletBuilder tb, Object[] arguments, List parameters, boolean negated) { @@ -237,7 +236,8 @@ public void apply(TacletBuilder tb, Object[] arguments, List paramete public static final AbstractConditionBuilder ARRAY = new ConstructorBasedBuilder("isArray", ArrayTypeCondition.class, SV); public static final AbstractConditionBuilder REFERENCE_ARRAY = - new AbstractConditionBuilder("isReferenceArray", SV) { + new AbstractConditionBuilder("isReferenceArray", ArrayComponentTypeCondition.class, true, + SV) { @Override public VariableCondition build(Object[] arguments, List parameters, boolean negated) { @@ -253,7 +253,7 @@ public VariableCondition build(Object[] arguments, List parameters, public static final AbstractConditionBuilder THIS_REFERENCE = new ConstructorBasedBuilder("isThisReference", IsThisReference.class, SV); public static final AbstractConditionBuilder REFERENCE = - new AbstractConditionBuilder("isReference", TR) { + new AbstractConditionBuilder("isReference", TypeCondition.class, true, TR) { @Override public VariableCondition build(Object[] arguments, List parameters, boolean negated) { @@ -303,8 +303,8 @@ public VariableCondition build(Object[] arguments, List parameters, static class JavaTypeToSortConditionBuilder extends AbstractConditionBuilder { private final boolean elmen; - public JavaTypeToSortConditionBuilder(@NonNull String triggerName, boolean forceElmentary) { - super(triggerName, SV, SORT); + public JavaTypeToSortConditionBuilder(String triggerName, boolean forceElmentary) { + super(triggerName, JavaTypeToSortCondition.class, false, SV, SORT); this.elmen = forceElmentary; } @@ -333,7 +333,7 @@ public VariableCondition build(Object[] arguments, List parameters, new ConstructorBasedBuilder("hasLabel", TermLabelCondition.class, TSV, S); // endregion public static final AbstractConditionBuilder STORE_TERM_IN = - new AbstractConditionBuilder("storeTermIn", SV, T) { + new AbstractConditionBuilder("storeTermIn", StoreTermInCondition.class, false, SV, T) { @Override public VariableCondition build(Object[] arguments, List parameters, boolean negated) { @@ -351,7 +351,7 @@ public VariableCondition build(Object[] arguments, List parameters, public static final AbstractConditionBuilder GET_FREE_INVARIANT = new ConstructorBasedBuilder( "\\getFreeInvariant", LoopFreeInvariantCondition.class, PV, SV, SV); public static final AbstractConditionBuilder GET_VARIANT = - new AbstractConditionBuilder("\\getVariant", PV, SV) { + new AbstractConditionBuilder("\\getVariant", LoopVariantCondition.class, false, PV, SV) { @Override public VariableCondition build(Object[] arguments, List parameters, boolean negated) { @@ -360,7 +360,7 @@ public VariableCondition build(Object[] arguments, List parameters, } }; public static final AbstractConditionBuilder IS_LABELED = - new AbstractConditionBuilder("isLabeled", PV) { + new AbstractConditionBuilder("isLabeled", IsLabeledCondition.class, true, PV) { @Override public IsLabeledCondition build(Object[] arguments, List parameters, boolean negated) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java new file mode 100644 index 00000000000..de15cc91730 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java @@ -0,0 +1,9 @@ +/** + * + * @author Alexander Weigl + * @version 1 (23.08.26) + */ +@NullMarked +package de.uka.ilkd.key.nparser.varexp; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java index 18d694523ae..b3c8e4b95a9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java @@ -6,10 +6,16 @@ import java.lang.reflect.Field; import java.lang.reflect.Modifier; -import java.util.*; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Comparator; +import java.util.List; import de.uka.ilkd.key.scripts.ProofScriptCommand; +import com.github.therapi.runtimejavadoc.ClassJavadoc; +import com.github.therapi.runtimejavadoc.FieldJavadoc; +import com.github.therapi.runtimejavadoc.RuntimeJavadoc; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -81,7 +87,7 @@ public static String generateCommandUsage(String commandName, Class parameter } public static String extractDocumentation(String command, Class commandClazz, - Class parameterClazz) { + @Nullable Class parameterClazz) { StringBuilder sb = new StringBuilder(); Deprecated dep = commandClazz.getAnnotation(Deprecated.class); @@ -90,22 +96,33 @@ public static String extractDocumentation(String command, Class commandClazz, "**Caution! This proof script command is deprecated, and may be removed soon!**\n\n"); } + ClassJavadoc jdocCommand = RuntimeJavadoc.getJavadoc(commandClazz); + Documentation docCommand = commandClazz.getAnnotation(Documentation.class); if (docCommand != null) { sb.append(docCommand.value()); sb.append("\n\n"); + } else { + sb.append(jdocCommand.getComment()); + sb.append("\n\n"); } if (parameterClazz == null) { return sb.toString(); } + ClassJavadoc jdocParams = RuntimeJavadoc.getJavadoc(parameterClazz); + Documentation docAn = parameterClazz.getAnnotation(Documentation.class); if (docAn != null) { sb.append(docAn.value()); sb.append("\n\n"); + } else { + sb.append(jdocParams.getComment()); + sb.append("\n\n"); } + sb.append("#### Usage: \n`").append(generateCommandUsage(command, parameterClazz)) .append("`\n\n"); @@ -114,13 +131,21 @@ public static String extractDocumentation(String command, Class commandClazz, sb.append("#### Parameters:\n"); for (ProofScriptArgument meta : args) { sb.append("\n\n"); + + var documentation = meta.getDocumentation(); + if (documentation.isEmpty()) { + documentation = jdocParams.getFields().stream() + .filter(it -> it.getName().equals(meta.getField().getName())) + .findFirst().map(FieldJavadoc::toString).orElse(""); + } + if (meta.isPositional()) { sb.append("* `%s` *(%s%s positional argument, type %s)*:
    %s".formatted( meta.getName(), meta.isRequired() ? "" : "optional ", ordinalStr(meta.getArgumentPosition() + 1), meta.getField().getType().getSimpleName(), - meta.getDocumentation())); + documentation)); } if (meta.isOption()) { @@ -128,28 +153,28 @@ public static String extractDocumentation(String command, Class commandClazz, meta.getName(), meta.isRequired() ? "" : "optional ", meta.getField().getType().getSimpleName(), - meta.getDocumentation())); + documentation)); } if (meta.isFlag()) { sb.append("* `%s` *(flag)*:
    %s".formatted( meta.getName(), - meta.getDocumentation())); + documentation)); } if (meta.isPositionalVarArgs()) { - sb.append("* `%s...` (%s): %s".formatted( + sb.append("* `%s...` (%s): %s
    %s".formatted( meta.getName(), meta.getPositionalVarargs().as(), meta.getPositionalVarargs().startIndex(), - meta.getDocumentation())); + documentation)); } if (meta.isOptionalVarArgs()) { sb.append("* `%s...`: *(options prefixed by `%s`, type %s)*:
    %s".formatted( meta.getName(), meta.getOptionalVarArgs().prefix(), meta.getOptionalVarArgs().as().getSimpleName(), - meta.getDocumentation())); + documentation)); } } @@ -189,39 +214,6 @@ public static String extractCategory(Class command private static @NonNull List getSortedProofScriptArguments( Class parameterClazz) { - // Comparator optional = - // Comparator.comparing(ProofScriptArgument::isOption); - // Comparator positional = - // Comparator.comparing(ProofScriptArgument::isPositional); - // Comparator flagal = - // Comparator.comparing(ProofScriptArgument::isFlag); - // Comparator allargsal = - // Comparator.comparing(ProofScriptArgument::isPositionalVarArgs); - // Comparator byRequired = - // Comparator.comparing(ProofScriptArgument::isRequired); - // Comparator byName = - // Comparator.comparing(ProofScriptArgument::getName); - // - // Comparator byPos = Comparator.comparing(it -> { - // if (it.isPositionalVarArgs()) { - // it.getPositionalVarargs().startIndex(); - // } - // if (it.isPositional()) { - // it.getArgument().value(); - // } - // - // return -1; - // }); - // - // - // var comp = optional - // .thenComparing(flagal) - // .thenComparing(positional) - // .thenComparing(allargsal) - // .thenComparing(byRequired) - // .thenComparing(byPos) - // .thenComparing(byName); - var args = Arrays.stream(parameterClazz.getDeclaredFields()) .map(ProofScriptArgument::new) .sorted(Comparator.comparing(ProofScriptArgument::orderString)) From 1c60671698084131da54255ab4c6e9a04dd9f748 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 14:48:09 +0200 Subject: [PATCH 02/11] Fix varcond negation detection breaking wd rule loading Determining whether a varcond implementation supports negation no longer matches the declared ArgumentType classes against the constructor's parameter types. The argument types are only coarse categories used for parsing and do not match the concrete parameter types (e.g. \isConstant expects an ArgumentType.VARIABLE, but ConstantCondition's constructor takes a JAbstractSortedOperator). A failed match made isNegationSupported throw an IllegalStateException, which was swallowed by TacletPBuilder's manipulator application, so the varcond could not be applied at all and taclet files using \isConstant or \hasLabel failed to load, breaking all key.core.wd run-all-proofs tests. The negation support check is restored to the previous lenient behavior: the first declared public constructor's last parameter must be boolean. Constructor lookup for documentation purposes now matches by parameter count and falls back to empty javadoc if the class was not processed by the therapi scribe. Also fix the warning in TacletPBuilder to print the argument types array instead of its identity. --- .../key/nparser/builder/TacletPBuilder.java | 2 +- .../varexp/TacletBuilderCommandInfo.java | 52 +++++++++++-------- 2 files changed, 30 insertions(+), 24 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 3aca30f2b35..9d0979d5650 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -801,7 +801,7 @@ public Object visitVarexp(JavaKeYParser.VarexpContext ctx) { } if (!applied) { LOGGER.warn("Found name-matching conditions with following type signature:"); - suitableManipulators.forEach(it -> LOGGER.warn(it.getArgumentTypes().toString())); + suitableManipulators.forEach(it -> LOGGER.warn(Arrays.toString(it.getArgumentTypes()))); LOGGER.warn("But you gave {} arguments.\n", arguments.size()); semanticError(ctx, "Could not apply the given variable condition: %s", ctx.getText()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java index 225fb5a1247..b170a0fcc26 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java @@ -163,7 +163,7 @@ public String[] argNames() { @Override public boolean isNegationSupported() { if (isNegationSupported == null) { - isNegationSupported = lastArgumentOfFirstConstructorIsBoolean(clazz, argTypes); + isNegationSupported = lastArgumentOfFirstConstructorIsBoolean(clazz); } return isNegationSupported; } @@ -201,6 +201,11 @@ Class[] getConstructorClasses() { /// instead of failing. private void findDocumentation() { ClassJavadoc classDoc = RuntimeJavadoc.getJavadoc(clazz.getName()); + if (classDoc == null) { + // The class was not processed by the therapi javadoc scribe; use empty + // documentation instead of failing. + classDoc = ClassJavadoc.createEmpty(clazz.getName()); + } generalDocumentation = classDoc; final var constr = findConstructor(clazz, getConstructorClasses()); @@ -234,38 +239,39 @@ private void findDocumentation() { } - /// Checks whether `clazz` declares a constructor whose parameter types are - /// `argTypes` followed by a trailing `boolean` parameter, which indicates - /// support for an optional negation flag. + /// Checks whether the first declared public constructor of `clazz` has a trailing + /// `boolean` parameter, which indicates support for an optional negation flag. + /// + /// Note: this check is intentionally lenient and does not try to match the declared + /// [ArgumentType]s against the constructor's parameter types. The argument types are + /// only categories used during parsing and only loosely approximate the actual + /// parameter types (e.g., `\isConstant` expects an [ArgumentType.VARIABLE] argument, + /// but `ConstantCondition`'s constructor takes a `JAbstractSortedOperator`). + /// A strict type-based matching would fail here and wrongly report "negation not + /// supported" or even throw, breaking the parsing of otherwise valid taclets. /// /// @param clazz the implementation class to inspect - /// @param argTypes the expected leading argument types /// @return `true` if such a constructor exists, `false` otherwise - /// @throws IllegalStateException if no suitable constructor exists in `clazz` - private static boolean lastArgumentOfFirstConstructorIsBoolean( - Class clazz, ArgumentType[] argTypes) { - if (findConstructor(clazz, getConstructorClasses(argTypes, true)) != null) { - return true; - } - if (findConstructor(clazz, getConstructorClasses(argTypes, false)) != null) { + private static boolean lastArgumentOfFirstConstructorIsBoolean(Class clazz) { + try { + Class[] types = clazz.getConstructors()[0].getParameterTypes(); + return types[types.length - 1] == Boolean.class + || types[types.length - 1] == Boolean.TYPE; + } catch (ArrayIndexOutOfBoundsException e) { return false; } - throw new IllegalStateException(); } + /// Looks up a constructor of `clazz` by the number of expected parameters. The + /// parameter types are deliberately not compared against the expected classes: + /// [ArgumentType]s only categorize the arguments for parsing and do not match the + /// concrete parameter types of the implementation classes. private static @Nullable Constructor findConstructor(Class clazz, Class[] constructorClasses) { final var constructors = clazz.getConstructors(); - c: for (var constructor : constructors) { - if (constructor.getParameterCount() != constructorClasses.length) - continue; - final var parameterTypes = constructor.getParameterTypes(); - for (var i = 0; i < parameterTypes.length; i++) { - if (!constructorClasses[i].isAssignableFrom(parameterTypes[i])) { - continue c; - } - } - return constructor; + for (var constructor : constructors) { + if (constructor.getParameterCount() == constructorClasses.length) + return constructor; } return null; } From 5b74d299cef0fefe750090045f8142fff0307658 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:04:44 +0200 Subject: [PATCH 03/11] key.core: reintroduce strict constructor type check for varcond builders Reintroduces the check that a varcond implementation constructor matches the declared ArgumentTypes, which was dropped as part of the initial fix for the wd proof tests. The negation-support detection is now tiered: a constructor whose parameter types are compatible with the declared argument types is preferred and decides negation support by its trailing boolean parameter. Only if no type-compatible constructor exists (the ArgumentType categories only approximate the real parameter types, as for \isConstant and \hasLabel), the previous lenient fallback on the first public constructor is retained. findConstructor (used for documentation lookup) prefers a type-compatible constructor and falls back to matching by parameter count. Verified: :key.core.wd:testRunAllWdProofs passes 9/9. --- .../varexp/TacletBuilderCommandInfo.java | 86 ++++++++++++++----- 1 file changed, 64 insertions(+), 22 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java index b170a0fcc26..01628f47cd6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java @@ -1,6 +1,7 @@ /* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.nparser.varexp; import java.lang.reflect.Constructor; @@ -163,7 +164,7 @@ public String[] argNames() { @Override public boolean isNegationSupported() { if (isNegationSupported == null) { - isNegationSupported = lastArgumentOfFirstConstructorIsBoolean(clazz); + isNegationSupported = lastArgumentOfFirstConstructorIsBoolean(clazz, argTypes); } return isNegationSupported; } @@ -239,20 +240,30 @@ private void findDocumentation() { } - /// Checks whether the first declared public constructor of `clazz` has a trailing - /// `boolean` parameter, which indicates support for an optional negation flag. + /// Determines whether the backing implementation class supports an optional trailing + /// negation flag, i.e. whether it has a constructor whose parameters are the declared + /// [`argument types`][#argumentTypes()] followed by an additional `boolean` parameter. /// - /// Note: this check is intentionally lenient and does not try to match the declared - /// [ArgumentType]s against the constructor's parameter types. The argument types are - /// only categories used during parsing and only loosely approximate the actual - /// parameter types (e.g., `\isConstant` expects an [ArgumentType.VARIABLE] argument, - /// but `ConstantCondition`'s constructor takes a `JAbstractSortedOperator`). - /// A strict type-based matching would fail here and wrongly report "negation not - /// supported" or even throw, breaking the parsing of otherwise valid taclets. + /// First, a constructor is searched whose parameter types are compatible with the + /// declared [ArgumentType]s; if that succeeds, the presence of the trailing `boolean` + /// decides negation support. If no type-compatible constructor can be found — the + /// [ArgumentType]s only loosely approximate the actual parameter types (e.g., + /// `\isConstant` declares an [ArgumentType.VARIABLE], but `ConstantCondition`'s + /// constructor takes a `JAbstractSortedOperator`) — the check falls back to the + /// original, lenient behavior: the last parameter of the first declared public + /// constructor must be a `boolean`. /// /// @param clazz the implementation class to inspect - /// @return `true` if such a constructor exists, `false` otherwise - private static boolean lastArgumentOfFirstConstructorIsBoolean(Class clazz) { + /// @param argTypes the declared argument types + /// @return `true` if negation is supported, `false` otherwise + private static boolean lastArgumentOfFirstConstructorIsBoolean( + Class clazz, ArgumentType[] argTypes) { + if (findTypedConstructor(clazz, getConstructorClasses(argTypes, true)) != null) { + return true; + } + if (findTypedConstructor(clazz, getConstructorClasses(argTypes, false)) != null) { + return false; + } try { Class[] types = clazz.getConstructors()[0].getParameterTypes(); return types[types.length - 1] == Boolean.class @@ -262,16 +273,47 @@ private static boolean lastArgumentOfFirstConstructorIsBoolean(Class clazz) { } } - /// Looks up a constructor of `clazz` by the number of expected parameters. The - /// parameter types are deliberately not compared against the expected classes: - /// [ArgumentType]s only categorize the arguments for parsing and do not match the - /// concrete parameter types of the implementation classes. + /// Searches a constructor of `clazz` whose parameter types are compatible with + /// `constructorClasses`: each actual parameter type must be assignable to the + /// expected class, i.e. be a subtype of it. + /// + /// @param clazz the implementation class to inspect + /// @param constructorClasses the expected parameter classes + /// @return the matching constructor, or `null` if none is type-compatible + private static @Nullable Constructor findTypedConstructor(Class clazz, + Class[] constructorClasses) { + c: for (var constructor : clazz.getConstructors()) { + if (constructor.getParameterCount() != constructorClasses.length) + continue; + final var parameterTypes = constructor.getParameterTypes(); + for (var i = 0; i < parameterTypes.length; i++) { + if (!constructorClasses[i].isAssignableFrom(parameterTypes[i])) { + continue c; + } + } + return constructor; + } + return null; + } + + /// Looks up a constructor of `clazz` for documentation purposes: a type-compatible + /// constructor is preferred; if none exists, a constructor with the same number of + /// parameters is used, since the [ArgumentType] classes only approximate the actual + /// parameter types. + /// + /// @param clazz the implementation class to inspect + /// @param constructorClasses the expected parameter classes + /// @return the best matching constructor, or `null` if none is found private static @Nullable Constructor findConstructor(Class clazz, Class[] constructorClasses) { - final var constructors = clazz.getConstructors(); - for (var constructor : constructors) { - if (constructor.getParameterCount() == constructorClasses.length) - return constructor; + var constructor = findTypedConstructor(clazz, constructorClasses); + if (constructor != null) { + return constructor; + } + for (var c : clazz.getConstructors()) { + if (c.getParameterCount() == constructorClasses.length) { + return c; + } } return null; } From 5a0210ed90488a89ed04af517cd26054fcf0c29d Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:04:49 +0200 Subject: [PATCH 04/11] key.core: complete missing Javadocs in documentation-relevant packages The documentation generators (VarcondDoc, ScriptDoc) extract Javadocs via therapi from de.uka.ilkd.key.rule.conditions and de.uka.ilkd.key.scripts. Complete the gaps so the generated documentation is not empty: - rule.conditions: add missing class documentation (ArrayLength, DifferentInstantiation, DropEffectlessElementaries, DropEffectlessStores, EqualUnique, FreeLabelIn, MetaDisjoint, Observer, SimplifyIfThenElseUpdate) and constructor documentation with @param descriptions for all variable condition implementations and TypeResolver's nested resolvers; fix the copy-pasted class documentation of IsThisReference. - scripts: document TermWithHoles and SequentWithHoles, fill the empty class documentation of the deprecated SchemaVarCommand, and add the missing class-level @Documentation to the Parameters classes of branches, expandDef, rewrite, and set. - normalize license headers to the spotless template (ScriptDoc, VarcondDoc, TacletBuilderCommandInfo). --- .../java/de/uka/ilkd/key/doc/ScriptDoc.java | 5 ++-- .../java/de/uka/ilkd/key/doc/VarcondDoc.java | 5 ++-- .../conditions/AbstractOrInterfaceType.java | 6 +++++ .../AlternativeVariableCondition.java | 6 +++++ .../rule/conditions/ArrayLengthCondition.java | 13 +++++++++ .../rule/conditions/ConstantCondition.java | 7 +++++ .../key/rule/conditions/DifferentFields.java | 7 +++++ .../DifferentInstantiationCondition.java | 12 +++++++++ .../DropEffectlessElementariesCondition.java | 15 +++++++++++ .../DropEffectlessStoresCondition.java | 17 ++++++++++++ .../rule/conditions/EqualUniqueCondition.java | 16 +++++++++++ .../conditions/FieldTypeToSortCondition.java | 7 +++++ .../key/rule/conditions/FinalTypeVarCond.java | 6 +++++ .../FreeLabelInVariableCondition.java | 14 ++++++++++ .../conditions/HasLoopInvariantCondition.java | 8 ++++++ .../ilkd/key/rule/conditions/InStrictFp.java | 5 ++++ .../rule/conditions/IsLabeledCondition.java | 7 +++++ .../key/rule/conditions/IsThisReference.java | 10 ++++++- .../conditions/JavaTypeToSortCondition.java | 8 ++++++ .../conditions/LocalVariableCondition.java | 8 ++++++ .../LoopFreeInvariantCondition.java | 9 +++++++ .../conditions/LoopInvariantCondition.java | 9 +++++++ .../rule/conditions/LoopVariantCondition.java | 7 +++++ .../conditions/MayExpandMethodCondition.java | 8 ++++++ .../conditions/MetaDisjointCondition.java | 12 +++++++++ .../rule/conditions/ModelFieldCondition.java | 6 +++++ .../conditions/NewJumpLabelCondition.java | 9 +++++++ .../conditions/NewLocalVarsCondition.java | 11 ++++++++ .../rule/conditions/ObserverCondition.java | 16 +++++++++++ .../SimplifyIfThenElseUpdateCondition.java | 19 ++++++++++++- .../rule/conditions/StaticFieldCondition.java | 6 +++++ .../rule/conditions/StoreStmtInCondition.java | 7 +++++ .../rule/conditions/StoreTermInCondition.java | 7 +++++ .../rule/conditions/SubFormulaCondition.java | 6 +++++ .../rule/conditions/TermLabelCondition.java | 7 +++++ .../key/rule/conditions/TypeResolver.java | 27 +++++++++++++++++++ .../uka/ilkd/key/scripts/BranchesCommand.java | 4 +++ .../ilkd/key/scripts/ExpandDefCommand.java | 3 +++ .../uka/ilkd/key/scripts/RewriteCommand.java | 3 +++ .../ilkd/key/scripts/SchemaVarCommand.java | 2 ++ .../ilkd/key/scripts/SequentWithHoles.java | 5 ++++ .../de/uka/ilkd/key/scripts/SetCommand.java | 4 +++ .../uka/ilkd/key/scripts/TermWithHoles.java | 6 +++++ 43 files changed, 369 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java index ae9d19210a5..529a3eb1d8c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java @@ -1,6 +1,7 @@ /* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.doc; import java.util.ArrayList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java index 08403ae95a2..9ae3cd9b717 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java @@ -1,6 +1,7 @@ /* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.doc; import java.util.Arrays; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java index 31cc211f35d..40892e17faa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java @@ -21,6 +21,12 @@ public final class AbstractOrInterfaceType extends VariableConditionAdapter { private final TypeResolver resolver; private final boolean negated; + /** + * Instantiates a new abstract-or-interface condition. + * + * @param tr the type resolver for the type to check + * @param negation whether the condition is negated ({@code \not isAbstractOrInterface}) + */ public AbstractOrInterfaceType(TypeResolver tr, boolean negation) { this.resolver = tr; this.negated = negation; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java index 9aa8df14667..99559995871 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java @@ -22,6 +22,12 @@ public final class AlternativeVariableCondition extends VariableConditionAdapter private final VariableConditionAdapter delegate0, delegate1; + /** + * Instantiates a new alternative (disjunction) of two variable conditions. + * + * @param delegate0 the first of the two conditions + * @param delegate1 the second of the two conditions + */ public AlternativeVariableCondition(VariableConditionAdapter delegate0, VariableConditionAdapter delegate1) { this.delegate0 = delegate0; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java index 039f9675eb6..238124fa313 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java @@ -15,12 +15,25 @@ import org.key_project.logic.op.sv.SchemaVariable; +/** + * A variable condition for the taclet construct {@code \isArrayLength}, checking that a schema + * variable is instantiated with the implicit array length attribute. + * + * @author Michael Kirsten + */ public final class ArrayLengthCondition extends VariableConditionAdapter { private final SchemaVariable reference; private final boolean negation; + /** + * Instantiates a new array length condition. + * + * @param reference the schema variable which must be instantiated with the array length + * attribute of some array type + * @param negation whether the condition is negated ({@code \not isArrayLength}) + */ public ArrayLengthCondition(SchemaVariable reference, boolean negation) { this.reference = reference; this.negation = negation; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java index 3181fde6b07..f938376ab5d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java @@ -26,6 +26,13 @@ public class ConstantCondition extends VariableConditionAdapter { private final JAbstractSortedOperator t; private final boolean negated; + /** + * Instantiates a new constant condition. + * + * @param t the term or formula schema variable which must be instantiated with a constant + * (zero-arity) term + * @param negated whether the condition is negated ({@code \not isConstant}) + */ public ConstantCondition(JAbstractSortedOperator t, boolean negated) { this.t = t; this.negated = negated; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java index a6f5910f3c1..4e94eb2934b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java @@ -22,6 +22,13 @@ public final class DifferentFields extends VariableConditionAdapter { private final SchemaVariable var1, var2; + /** + * Instantiates a new different-fields condition. + * + * @param var1 the first schema variable; both instantiations must differ in their top-level + * unique function symbol + * @param var2 the second schema variable + */ public DifferentFields(SchemaVariable var1, SchemaVariable var2) { this.var1 = var1; this.var2 = var2; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java index 187b5132bf1..d3a81a81284 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java @@ -13,10 +13,22 @@ import org.key_project.logic.op.sv.SchemaVariable; +/** + * A variable condition for the taclet construct {@code \different}, ensuring that two schema + * variables are instantiated with distinct elements. + * + * @author Michael Kirsten + */ public final class DifferentInstantiationCondition extends VariableConditionAdapter { private final SchemaVariable var1, var2; + /** + * Instantiates a new different-instantiation condition. + * + * @param var1 the first schema variable + * @param var2 the second schema variable; both must not be instantiated with the same element + */ public DifferentInstantiationCondition(SchemaVariable var1, SchemaVariable var2) { this.var1 = var1; this.var2 = var2; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java index 9e714dd60de..a0ddf1788bb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java @@ -27,11 +27,26 @@ import org.key_project.prover.rules.instantiation.MatchResultInfo; +/** + * A variable condition for the taclet construct {@code \dropEffectlessElementaries}: given an + * update and a target term, it computes the update with all elementary updates removed that do not + * affect (are not "relevant" for) the target term, and binds the result to a third schema variable. + * + * @author Michael Kirsten + */ public final class DropEffectlessElementariesCondition implements VariableCondition { private final UpdateSV u; private final SchemaVariable x; private final SchemaVariable result; + /** + * Instantiates a new drop-effectless-elementaries condition. + * + * @param u the update schema variable whose instantiation is simplified + * @param x the schema variable holding the target term which determines the relevant locations + * @param x2 the schema variable to which the simplified update application + * {@code u(x)} is bound + */ public DropEffectlessElementariesCondition(UpdateSV u, SchemaVariable x, SchemaVariable x2) { this.u = u; this.x = x; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java index 9aad185f8ea..02769045351 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java @@ -23,6 +23,13 @@ import org.key_project.util.collection.Pair; +/** + * A variable condition for the taclet construct {@code \dropEffectlessStores}: it removes all + * {@code store} operations from a heap term that are overwritten by later {@code store} operations + * on the same location, and binds the simplified heap to a result schema variable. + * + * @author Michael Kirsten + */ public final class DropEffectlessStoresCondition implements VariableCondition { private final TermSV h; private final TermSV o; @@ -30,6 +37,16 @@ public final class DropEffectlessStoresCondition implements VariableCondition { private final TermSV x; private final TermSV result; + /** + * Instantiates a new drop-effectless-stores condition. + * + * @param h the term schema variable for the heap on which the store operation is performed + * @param o the term schema variable for the object of the store operation + * @param f the term schema variable for the field of the store operation + * @param x the term schema variable for the value written by the store operation + * @param result the term schema variable to which the heap with all effectless stores removed + * is bound + */ public DropEffectlessStoresCondition(TermSV h, TermSV o, TermSV f, TermSV x, TermSV result) { this.h = h; this.o = o; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java index 479d698190a..5d224fc122c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java @@ -19,12 +19,28 @@ import org.key_project.prover.rules.instantiation.MatchResultInfo; +/** + * A variable condition for the taclet construct {@code \equalUnique}: checks that two term schema + * variables are instantiated with (distinct) applications of functions marked as {@code unique}, + * and if so binds a formula schema variable to the equation of both terms. + * + * @author Michael Kirsten + */ public final class EqualUniqueCondition implements VariableCondition { private final TermSV t; private final TermSV t2; private final FormulaSV res; + /** + * Instantiates a new equal-unique condition. + * + * @param t the first term schema variable; its instantiation must be the application of a + * unique function + * @param t2 the second term schema variable; its instantiation must be the application of a + * unique function + * @param res the formula schema variable to which the equation {@code t = t2} is bound + */ public EqualUniqueCondition(TermSV t, TermSV t2, FormulaSV res) { this.t = t; this.t2 = t2; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java index 3aac2f76438..fbc5cf47584 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java @@ -34,6 +34,13 @@ public final class FieldTypeToSortCondition implements VariableCondition { private final SchemaVariable exprOrTypeSV; private final GenericSort sort; + /** + * Instantiates a new field-type condition. + * + * @param exprOrTypeSV the expression or type schema variable whose instantiation must be a + * field constant + * @param sort the generic sort which is instantiated with the referred type of the field + */ public FieldTypeToSortCondition(final JOperatorSV exprOrTypeSV, final GenericSort sort) { this.exprOrTypeSV = exprOrTypeSV; this.sort = sort; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java index 1e70a06df11..8ca23730f80 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java @@ -30,6 +30,12 @@ public final class FinalTypeVarCond extends VariableConditionAdapter { private final TypeResolver resolver; private final boolean negated; + /** + * Instantiates a new final-type condition. + * + * @param tr the type resolver for the type to check + * @param negation whether the condition is negated ({@code \not isFinal}) + */ public FinalTypeVarCond(TypeResolver tr, boolean negation) { this.resolver = tr; this.negated = negation; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java index 8cb9d637c9e..3036ca51a6a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java @@ -15,6 +15,12 @@ import org.key_project.logic.op.sv.SchemaVariable; +/** + * A variable condition for the taclet construct {@code \freeLabelIn}, checking whether a program + * label occurs freely in a Java program (block). + * + * @author Michael Kirsten + */ public final class FreeLabelInVariableCondition extends VariableConditionAdapter { private final SchemaVariable label; @@ -22,6 +28,14 @@ public final class FreeLabelInVariableCondition extends VariableConditionAdapter private final boolean negated; private final FreeLabelFinder freeLabelFinder = new FreeLabelFinder(); + /** + * Instantiates a new free-label-in condition. + * + * @param label the schema variable which must be instantiated with a program label + * @param statement the schema variable which must be instantiated with a program element + * (statement) + * @param negated whether the condition is negated ({@code \not freeLabelIn}) + */ public FreeLabelInVariableCondition(SchemaVariable label, SchemaVariable statement, boolean negated) { this.label = label; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java index ed8cbf111b1..26eb90ef761 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java @@ -35,6 +35,14 @@ public class HasLoopInvariantCondition implements VariableCondition { private final ProgramSV loopStmtSV; private final SchemaVariable modalitySV; + /** + * Instantiates a new has-loop-invariant condition. + * + * @param loopStmtSV the program schema variable which must be instantiated with a loop + * statement + * @param modalitySV the schema variable for the modality kind determining the applicable heap + * context + */ public HasLoopInvariantCondition(ProgramSV loopStmtSV, SchemaVariable modalitySV) { this.loopStmtSV = loopStmtSV; this.modalitySV = modalitySV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java index 3a109b01923..72a58a73056 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java @@ -23,6 +23,11 @@ public final class InStrictFp extends VariableConditionAdapter { private final boolean negated; + /** + * Instantiates a new strict-fp condition. + * + * @param negation whether the condition is negated ({@code \not isInStrictFp}) + */ public InStrictFp(boolean negation) { this.negated = negation; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java index a572aa2c281..0a16db06fb9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java @@ -29,6 +29,13 @@ public class IsLabeledCondition implements VariableCondition { private final boolean negated; private final ProgramSV stmtSV; + /** + * Instantiates a new is-labeled condition. + * + * @param stmtSV the program schema variable which must be instantiated with a labeled + * statement + * @param negated whether the condition is negated ({@code \not isLabeled}) + */ public IsLabeledCondition(ProgramSV stmtSV, boolean negated) { this.stmtSV = stmtSV; this.negated = negated; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java index 973ae44c29e..5e790c5a459 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java @@ -17,13 +17,21 @@ /** - * This variable condition checks if a given type denotes an abstract class or interface type. + * This variable condition checks if a program variable is instantiated with a {@code this} + * reference. */ public final class IsThisReference extends VariableConditionAdapter { private final boolean negated; private final ParsableVariable var; + /** + * Instantiates a new this-reference condition. + * + * @param var the program schema variable which must be instantiated with a {@code this} + * reference + * @param negation whether the condition is negated ({@code \not isThisReference}) + */ public IsThisReference(ParsableVariable var, boolean negation) { this.negated = negation; this.var = var; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java index 1a2c856b070..208210d7a81 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java @@ -36,6 +36,14 @@ public final class JavaTypeToSortCondition implements VariableCondition { private final boolean elemSort; + /** + * Instantiates a new java-type-to-sort condition. + * + * @param exprOrTypeSV the expression or type schema variable whose instantiation determines + * the sort + * @param sort the generic sort which is instantiated with the sort of the instantiation + * @param elemSort whether the elementary sort is to be used for array types + */ public JavaTypeToSortCondition(final JOperatorSV exprOrTypeSV, final GenericSort sort, final boolean elemSort) { this.exprOrTypeSV = exprOrTypeSV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java index 7234a7bddf7..b11432ab50f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java @@ -22,6 +22,14 @@ public final class LocalVariableCondition extends VariableConditionAdapter { private final SchemaVariable var; private final boolean neg; + /** + * Instantiates a new local-variable condition. + * + * @param var the schema variable which must be instantiated with a local (non-member) program + * variable + * @param neg whether the condition is negated ({@code \not isLocalVariable}) + * @throws IllegalArgumentException if the given schema variable is not a {@link ProgramSV} + */ public LocalVariableCondition(SchemaVariable var, boolean neg) { this.var = var; this.neg = neg; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java index f7f1ed52f3c..2707f55bb3b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java @@ -38,6 +38,15 @@ public class LoopFreeInvariantCondition implements VariableCondition { private final SchemaVariable modalitySV; private final SchemaVariable invSV; + /** + * Instantiates a new free-loop-invariant condition. + * + * @param loopStmtSV the program schema variable which must be instantiated with a loop + * statement + * @param modalitySV the schema variable for the modality kind determining the applicable heap + * context + * @param invSV the schema variable to which the free loop invariant is bound + */ public LoopFreeInvariantCondition(ProgramSV loopStmtSV, SchemaVariable modalitySV, SchemaVariable invSV) { this.loopStmtSV = loopStmtSV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java index 833f4e1ccb7..fad27789b67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java @@ -37,6 +37,15 @@ public class LoopInvariantCondition implements VariableCondition { private final SchemaVariable modalitySV; private final SchemaVariable invSV; + /** + * Instantiates a new loop-invariant condition. + * + * @param loopStmtSV the program schema variable which must be instantiated with a loop + * statement + * @param modalitySV the schema variable for the modality kind determining the applicable heap + * context + * @param invSV the schema variable to which the loop invariant is bound + */ public LoopInvariantCondition(ProgramSV loopStmtSV, SchemaVariable modalitySV, SchemaVariable invSV) { this.loopStmtSV = loopStmtSV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java index fc23a3bbd37..7e515e0d8a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java @@ -26,6 +26,13 @@ public class LoopVariantCondition implements VariableCondition { private final SchemaVariable loopStmtSV; private final SchemaVariable variantSV; + /** + * Instantiates a new loop-variant condition. + * + * @param loopStmtSV the program schema variable which must be instantiated with a loop + * statement + * @param variantSV the schema variable to which the loop variant is bound + */ public LoopVariantCondition(ProgramSV loopStmtSV, SchemaVariable variantSV) { this.loopStmtSV = loopStmtSV; this.variantSV = variantSV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java index d2a5b206b84..b3d4256a218 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java @@ -95,6 +95,14 @@ public MayExpandMethodCondition(SchemaVariable receiver, SchemaVariable methname this.args = args; } + /** + * Instantiate a new variable condition for class-local method calls without an explicit + * receiver. + * + * @param methodName non-null program schema var for the methodname + * @param args non-null program schema var for the arguments of the call + * @param negation {@code true} iff the condition is to be negated + */ public MayExpandMethodCondition(SchemaVariable methodName, SchemaVariable args, boolean negation) { this(null, methodName, args, negation); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java index 051650ad602..a6c7a12bb56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java @@ -19,12 +19,24 @@ import org.key_project.util.collection.ImmutableSet; +/** + * A variable condition for the taclet construct {@code \metaDisjoint}, checking that the two + * instantiations of the given term schema variables denote provably disjoint location sets. + * + * @author Michael Kirsten + */ public final class MetaDisjointCondition extends VariableConditionAdapter { private final TermSV var1; private final TermSV var2; + /** + * Instantiates a new meta-disjoint condition. + * + * @param s1 the first term schema variable; its instantiation is interpreted as a location set + * @param s2 the second term schema variable; its instantiation is interpreted as a location set + */ public MetaDisjointCondition(TermSV s1, TermSV s2) { this.var1 = s1; this.var2 = s2; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java index e8c2e4376c9..4adda6d3749 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java @@ -43,6 +43,12 @@ public class ModelFieldCondition extends VariableConditionAdapter { private final SchemaVariable field; private final boolean negated; + /** + * Instantiates a new model-field condition. + * + * @param field the schema variable which must be instantiated with a Java field + * @param negated whether the condition is negated ({@code \not isModelField}) + */ public ModelFieldCondition(SchemaVariable field, boolean negated) { this.field = field; this.negated = negated; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java index c6f426a1a43..66a0e621ec9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java @@ -30,6 +30,15 @@ public final class NewJumpLabelCondition implements VariableCondition { private final ProgramSV labelSV; + /** + * Instantiates a new jump-label condition. + * + * @param sv the program schema variable of sort {@code LABEL} which must be instantiated with + * a label not occurring elsewhere in the context program or the schema variable + * instantiations + * @throws IllegalArgumentException if the given schema variable is not a program schema + * variable of sort {@code LABEL} + */ public NewJumpLabelCondition(SchemaVariable sv) { if (!(sv instanceof ProgramSV psv) || psv.sort() != ProgramSVSort.LABEL) { throw new IllegalArgumentException( diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java index 3b35c3f71c2..c022d91d3fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java @@ -61,6 +61,17 @@ public class NewLocalVarsCondition implements VariableCondition { */ private final SchemaVariable bodySV; + /** + * Instantiates a new local-variables condition. + * + * @param varDeclsSV the schema variable to which the variable declarations for the "before" + * versions of the variables written by the loop are bound + * @param updateBeforeSV the schema variable to which the update + * {@code {...||i_before := i||...}} is bound + * @param updateFrameSV the schema variable to which the reverse update + * {@code {...||i := i_before||...}} is bound + * @param bodySV the schema variable holding the loop body + */ public NewLocalVarsCondition(SchemaVariable varDeclsSV, SchemaVariable updateBeforeSV, SchemaVariable updateFrameSV, SchemaVariable bodySV) { this.varDeclsSV = varDeclsSV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java index e30eaa52b16..d340d97dcc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java @@ -17,12 +17,28 @@ import org.key_project.prover.rules.instantiation.SVInstantiations; +/** + * A variable condition for the taclet construct {@code \isObserver}, checking that a term schema + * variable is instantiated with an observer function and that the heap argument of the observer is + * the given heap term. If the heap schema variable is not yet instantiated, it is bound to the + * observer's heap argument. + * + * @author Michael Kirsten + */ public final class ObserverCondition implements VariableCondition { private final TermSV obs; private final TermSV heap; + /** + * Instantiates a new observer condition. + * + * @param obs the term schema variable which must be instantiated with an observer function + * application (an {@link IObserverFunction}) + * @param heap the term schema variable for the heap on which the observer is evaluated; it is + * automatically instantiated with the observer's heap argument if not yet instantiated + */ public ObserverCondition(TermSV obs, TermSV heap) { this.obs = obs; this.heap = heap; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java index d5ee7e09bb8..040833bb0f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java @@ -23,6 +23,14 @@ import org.key_project.prover.rules.instantiation.MatchResultInfo; import org.key_project.prover.rules.instantiation.SVInstantiations; +/** + * A variable condition for the taclet construct {@code \simplifyIfThenElseUpdate}: it turns two + * updates guarded by a condition {@code phi} into a single parallel update whose right-hand sides + * are {@code if phi then r1 else r2} expressions, and binds the common condition to a formula + * schema variable. + * + * @author Michael Kirsten + */ public class SimplifyIfThenElseUpdateCondition implements VariableCondition { private final FormulaSV phi; @@ -32,7 +40,16 @@ public class SimplifyIfThenElseUpdateCondition implements VariableCondition { private final SchemaVariable result; - + /** + * Instantiates a new simplify-if-then-else-update condition. + * + * @param phi the formula schema variable guarding the two updates + * @param u1 the update schema variable applied if {@code phi} holds + * @param u2 the update schema variable applied if {@code phi} does not hold + * @param commonFormula the formula schema variable to which the guard {@code phi} is bound + * @param result the schema variable to which the merged update + * {@code if phi then u1 else u2} is bound + */ public SimplifyIfThenElseUpdateCondition(FormulaSV phi, UpdateSV u1, UpdateSV u2, FormulaSV commonFormula, SchemaVariable result) { super(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java index ec55d75549b..1d463b661de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java @@ -31,6 +31,12 @@ public class StaticFieldCondition extends VariableConditionAdapter { private final SchemaVariable field; private final boolean negated; + /** + * Instantiates a new static-field condition. + * + * @param field the schema variable which must be instantiated with a Java field + * @param negated whether the condition is negated ({@code \not isStaticField}) + */ public StaticFieldCondition(SchemaVariable field, boolean negated) { this.field = field; this.negated = negated; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java index 3cd28c7f4c9..6f92a1e43db 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java @@ -34,6 +34,13 @@ public class StoreStmtInCondition implements VariableCondition { private final ProgramSV storeInSV; private final JTerm term; + /** + * Instantiates a new store-statement-in condition. + * + * @param resultVarSV the program schema variable to which the extracted statement is bound + * @param term the term whose Java block contains the statement to store; the statement is + * substituted with the current schema variable instantiations first + */ public StoreStmtInCondition(ProgramSV resultVarSV, JTerm term) { this.storeInSV = resultVarSV; this.term = term; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java index 80df4473aa3..b15377be4ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java @@ -25,6 +25,13 @@ public class StoreTermInCondition implements VariableCondition { private final SchemaVariable storeInSV; private final JTerm term; + /** + * Instantiates a new store-term-in condition. + * + * @param resultVarSV the schema variable to which the (substituted) term is bound + * @param term the term to store; it is substituted with the current schema variable + * instantiations first + */ public StoreTermInCondition(SchemaVariable resultVarSV, JTerm term) { this.storeInSV = resultVarSV; this.term = term; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java index 686c5040e07..ad9a021f944 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java @@ -28,6 +28,12 @@ public class SubFormulaCondition extends VariableConditionAdapter { private final FormulaSV a; private final boolean negated; + /** + * Instantiates a new sub-formula condition. + * + * @param a the formula schema variable whose instantiation is checked for formula sub-terms + * @param negated whether the condition is negated ({@code \not hasSubFormulas}) + */ public SubFormulaCondition(FormulaSV a, boolean negated) { this.a = a; this.negated = negated; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java index 3d2ad379330..45176d2bb21 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java @@ -27,6 +27,13 @@ public class TermLabelCondition extends VariableConditionAdapter { private final Name ln; private final boolean negated; + /** + * Instantiates a new term-label condition. + * + * @param l the term-label schema variable whose instantiations are searched for the label + * @param t the name of the term label to look for + * @param negated whether the condition is negated ({@code \not hasLabel}) + */ public TermLabelCondition(TermLabelSV l, String t, boolean negated) { this.l = l; this.ln = new Name(t); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index 504137f765e..6d7e09c7217 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -71,6 +71,11 @@ public static class GenericSortResolver extends TypeResolver { private final GenericSort gs; + /** + * Instantiates a new resolver for the instantiation of a generic sort. + * + * @param gs the generic sort whose instantiation is resolved + */ public GenericSortResolver(GenericSort gs) { this.gs = gs; } @@ -101,6 +106,11 @@ public static class NonGenericSortResolver extends TypeResolver { private final Sort s; + /** + * Instantiates a new resolver for a non-generic (concrete) sort. + * + * @param s the sort to resolve + */ public NonGenericSortResolver(Sort s) { this.s = s; } @@ -131,6 +141,12 @@ public static class ElementTypeResolverForSV extends TypeResolver { private final SchemaVariable resolveSV; + /** + * Instantiates a new resolver for the element type of the instantiation of a schema + * variable. + * + * @param sv the schema variable whose instantiation's element type is resolved + */ public ElementTypeResolverForSV(SchemaVariable sv) { this.resolveSV = sv; } @@ -179,6 +195,12 @@ public static class ContainerTypeResolver extends TypeResolver { private final SchemaVariable memberSV; + /** + * Instantiates a new resolver for the container type of the instantiation of a schema + * variable. + * + * @param sv the schema variable whose instantiation's container type is resolved + */ public ContainerTypeResolver(SchemaVariable sv) { this.memberSV = sv; } @@ -243,6 +265,11 @@ public String toString() { private static class ParametricSortResolver extends TypeResolver { private final ParametricSortInstance psi; + /** + * Instantiates a new resolver for the instantiation of a parametric sort instance. + * + * @param psi the parametric sort instance whose instantiation is resolved + */ public ParametricSortResolver(ParametricSortInstance psi) { this.psi = psi; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java index 89590cfdf0d..4e0d6993027 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java @@ -176,6 +176,10 @@ private Node findNodeByNumber(Proof proof, int serial) throws ScriptException { throw new ScriptException(); } + @Documentation(category = "Auxiliary", value = """ + Selects or removes a branch in the proof tree, or restricts the automatic strategy + to a selected branch. + """) public static class Parameters { @Argument @Documentation("The operation mode: 'push', 'pop', 'select', or 'single'") diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java index ada1dc76f1f..3619594161f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java @@ -122,6 +122,9 @@ private TacletApp makeRuleApp(Parameters p, EngineState state) throws ScriptExce } + @Documentation(category = "Auxiliary", value = """ + Expands method and class invariant definitions at a given location in the goal. + """) public static class Parameters { @Option(value = "on") @Documentation("A term pattern to match the expansion location against") diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java index 1b7462e992a..09c98b6a3ef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java @@ -252,6 +252,9 @@ private JTerm getSubTerm(JTerm t, IntIterator pit) { } } + @Documentation(category = "Auxiliary", value = """ + Rewrites all occurrences of a term pattern into a replacement term. + """) public static class Parameters { @Option(value = "find") @Documentation("The term pattern to search for and replace") diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java index a03deed85fe..32b1770d101 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java @@ -18,7 +18,9 @@ import org.checkerframework.checker.nullness.qual.MonotonicNonNull; /** + * Defines a schema variable that can be used in subsequent script commands. * + * @deprecated use the abbreviation mechanism of the KeY parser instead. */ @Deprecated public class SchemaVarCommand extends AbstractCommand { diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java index 8ff63cf5291..de90d176f04 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java @@ -20,6 +20,11 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +/// A sequent whose antecedent and succedent formulas may contain holes (placeholders). +/// It is used to express term patterns with holes in proof script commands, which are +/// matched against (parts of) the current goals. +/// +/// @author Alexander Weigl @NullMarked public class SequentWithHoles { diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java index 8a55d458608..0d60d135aa5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java @@ -168,6 +168,10 @@ public String getName() { return "set"; } + @Documentation(category = "Control", value = """ + Configures the automatic strategy and further proof settings by assigning + key-value pairs, e.g. `set oss false` or `set steps 100`. + """) public static class Parameters { @Documentation("Enable/disable one-step simplification") diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java index 30e9e65265b..b2b4cf8d87b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java @@ -38,6 +38,12 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +/// A term that may contain holes (wildcards) and focus or ellipsis markers, written with +/// the placeholders `?` (term hole), `?fml` (formula hole), `?focus` (focus point) and +/// `?find` (ellipsis). Such patterns are used by proof script commands (e.g. `rewrite`, +/// `expand`, `focus`) to match terms and formulas of the current goal. +/// +/// @author Alexander Weigl @NullMarked public class TermWithHoles { From 758c9f7d6437b30901bcabd1480e1994565351d3 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:20:08 +0200 Subject: [PATCH 05/11] CI, key.core: generate varcond/proof-script documentation in nightly build Add the Gradle tasks generateVarcondDoc and generateScriptDoc, which run the documentation generators (VarcondDoc, ScriptDoc) and write the resulting markdown to key.core/build/docs/keydocs. The nightly workflow additionally sets up JDK 25 for the generation step (therapi's scribe only extracts '///' markdown javadocs on JDK 23+), packages the generated files and uploads them as the artifact "varcond-script-docs" with a retention of 30 days. --- .github/workflows/nightlydeploy.yml | 22 +++++++++++++++++++ key.core/build.gradle | 34 +++++++++++++++++++++++++++++ 2 files changed, 56 insertions(+) diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 953ee83037a..dbb14ab2bc8 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -80,3 +80,25 @@ jobs: ORG_GRADLE_PROJECT_signingInMemoryKeyPassword: ${{secrets.GPG_PASSPHRASE}} ORG_GRADLE_PROJECT_mavenCentralUsername: ${{ secrets.SONATYPE_USERNAME }} ORG_GRADLE_PROJECT_mavenCentralPassword: ${{ secrets.SONATYPE_PASSWORD }} + + # The documentation generation for varconds and proof script commands + # extracts `///` markdown javadocs via therapi, which requires JDK 23+. + - name: Set up JDK 25 (documentation generation) + uses: actions/setup-java@v6.0.1 + with: + java-version: '25' + distribution: 'temurin' + cache: 'gradle' + + - name: Generate varcond and proof script documentation + run: ./gradlew --parallel :key.core:generateVarcondDoc :key.core:generateScriptDoc + + - name: Package varcond and proof script documentation + run: tar cvf key-varcond-script-docs.tar.xz -C key.core/build/docs/keydocs . + + - name: Upload varcond and proof script documentation + uses: actions/upload-artifact@v7 + with: + name: varcond-script-docs + path: "key-varcond-script-docs.tar.xz" + retention-days: 30 diff --git a/key.core/build.gradle b/key.core/build.gradle index 7567393c7fb..3015d80e79c 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -70,6 +70,40 @@ tasks.register('generateSMTListings') { } } +def keyScriptDocsDir = layout.buildDirectory.dir("docs/keydocs") + +// Generates the markdown documentation of all variable conditions (varconds), +// see de.uka.ilkd.key.doc.VarcondDoc. +tasks.register('generateVarcondDoc', JavaExec) { + group = 'documentation' + description = 'Generates the markdown documentation of all variable conditions (varconds).' + classpath = sourceSets.main.runtimeClasspath + mainClass = 'de.uka.ilkd.key.doc.VarcondDoc' + def outputFile = layout.buildDirectory.file("docs/keydocs/varconds.md") + outputs.file(outputFile) + doFirst { + def f = outputFile.get().asFile + f.parentFile.mkdirs() + standardOutput = new FileOutputStream(f) + } +} + +// Generates the markdown documentation of all proof script commands, +// see de.uka.ilkd.key.doc.ScriptDoc. +tasks.register('generateScriptDoc', JavaExec) { + group = 'documentation' + description = 'Generates the markdown documentation of all proof script commands.' + classpath = sourceSets.main.runtimeClasspath + mainClass = 'de.uka.ilkd.key.doc.ScriptDoc' + def outputFile = layout.buildDirectory.file("docs/keydocs/script-commands.md") + outputs.file(outputFile) + doFirst { + def f = outputFile.get().asFile + f.parentFile.mkdirs() + standardOutput = new FileOutputStream(f) + } +} + tasks.register('generateSolverPropsList') { def pack = "de/uka/ilkd/key/smt/solvertypes" def resourcesDir = "${project.projectDir}/src/main/resources" From de89eb05378a8c98e03ec5592c26ad225635df2e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:20:10 +0200 Subject: [PATCH 06/11] key.core: fix documentation generation crashes and raw javadoc output - ArgumentsLifter: null-guard the therapi javadoc lookups, which return null for classes compiled with a JDK that does not recognize the used doc comment style, and format field javadoc comments with the CommentFormatter instead of printing the raw FieldJavadoc object. - TacletBuilderCommandInfoImpl: bound the @param name lookup by the documented parameter count, which may be shorter than the declared argument types. --- .../nparser/varexp/TacletBuilderCommandInfo.java | 4 ++-- .../uka/ilkd/key/scripts/meta/ArgumentsLifter.java | 14 +++++++++----- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java index 01628f47cd6..9287004aead 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java @@ -223,13 +223,13 @@ private void findDocumentation() { final var parameters = constr.getParameters(); argNames = new String[argTypes.length]; - for (int i = 0; i < argTypes.length; i++) { + for (int i = 0; i < argTypes.length && i < parameters.length; i++) { argNames[i] = parameters[i].getName(); } constructorDeclaration.ifPresent(it -> { List params = it.getParams(); - for (int i = 0; i < argNames.length; i++) { + for (int i = 0; i < argNames.length && i < params.size(); i++) { argNames[i] = params.get(i).getName(); } }); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java index b3c8e4b95a9..70992d6905b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.scripts.ProofScriptCommand; import com.github.therapi.runtimejavadoc.ClassJavadoc; -import com.github.therapi.runtimejavadoc.FieldJavadoc; +import com.github.therapi.runtimejavadoc.CommentFormatter; import com.github.therapi.runtimejavadoc.RuntimeJavadoc; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -102,7 +102,9 @@ public static String extractDocumentation(String command, Class commandClazz, if (docCommand != null) { sb.append(docCommand.value()); sb.append("\n\n"); - } else { + } else if (jdocCommand != null && jdocCommand.getComment() != null) { + // the javadoc is only available if the class was compiled with a JDK that + // understands the doc comment style used in the source (e.g., JDK 23+ for ///) sb.append(jdocCommand.getComment()); sb.append("\n\n"); } @@ -117,7 +119,7 @@ public static String extractDocumentation(String command, Class commandClazz, if (docAn != null) { sb.append(docAn.value()); sb.append("\n\n"); - } else { + } else if (jdocParams != null && jdocParams.getComment() != null) { sb.append(jdocParams.getComment()); sb.append("\n\n"); } @@ -133,10 +135,12 @@ public static String extractDocumentation(String command, Class commandClazz, sb.append("\n\n"); var documentation = meta.getDocumentation(); - if (documentation.isEmpty()) { + if (documentation.isEmpty() && jdocParams != null) { documentation = jdocParams.getFields().stream() .filter(it -> it.getName().equals(meta.getField().getName())) - .findFirst().map(FieldJavadoc::toString).orElse(""); + .findFirst() + .map(field -> new CommentFormatter().format(field.getComment())) + .orElse(""); } if (meta.isPositional()) { From 1f10264234e2189fbd9b087dc34177f0ab9ce0a5 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:22:05 +0200 Subject: [PATCH 07/11] CI: package generated key documentation as zip --- .github/workflows/nightlydeploy.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index dbb14ab2bc8..a8484f91bb5 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -94,11 +94,11 @@ jobs: run: ./gradlew --parallel :key.core:generateVarcondDoc :key.core:generateScriptDoc - name: Package varcond and proof script documentation - run: tar cvf key-varcond-script-docs.tar.xz -C key.core/build/docs/keydocs . + run: zip -j key-varcond-script-docs.zip key.core/build/docs/keydocs/* - name: Upload varcond and proof script documentation uses: actions/upload-artifact@v7 with: name: varcond-script-docs - path: "key-varcond-script-docs.tar.xz" + path: "key-varcond-script-docs.zip" retention-days: 30 From 5a91fd556811ec7966eb4b42ea4d6170cb6e832e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:27:50 +0200 Subject: [PATCH 08/11] key.core: share doc-generator functionality between VarcondDoc and ScriptDoc Extract the common functionality of the documentation generators into the new base class AbstractDocGenerator: - output handling: the generators write to stdout, or to the file given as the first command line argument (creating missing directories), which simplifies the Gradle tasks generateVarcondDoc/generateScriptDoc - javadoc post-processing: cleanJavadoc and indent are moved here and are now also applied by ScriptDoc - ScriptDoc additionally prints a section header per command, matching the format of VarcondDoc --- key.core/build.gradle | 10 +-- .../ilkd/key/doc/AbstractDocGenerator.java | 86 +++++++++++++++++++ .../java/de/uka/ilkd/key/doc/ScriptDoc.java | 19 +++- .../java/de/uka/ilkd/key/doc/VarcondDoc.java | 66 +++++--------- 4 files changed, 125 insertions(+), 56 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java diff --git a/key.core/build.gradle b/key.core/build.gradle index 3015d80e79c..1fce543f748 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -70,8 +70,6 @@ tasks.register('generateSMTListings') { } } -def keyScriptDocsDir = layout.buildDirectory.dir("docs/keydocs") - // Generates the markdown documentation of all variable conditions (varconds), // see de.uka.ilkd.key.doc.VarcondDoc. tasks.register('generateVarcondDoc', JavaExec) { @@ -82,9 +80,7 @@ tasks.register('generateVarcondDoc', JavaExec) { def outputFile = layout.buildDirectory.file("docs/keydocs/varconds.md") outputs.file(outputFile) doFirst { - def f = outputFile.get().asFile - f.parentFile.mkdirs() - standardOutput = new FileOutputStream(f) + args = [outputFile.get().asFile.absolutePath] } } @@ -98,9 +94,7 @@ tasks.register('generateScriptDoc', JavaExec) { def outputFile = layout.buildDirectory.file("docs/keydocs/script-commands.md") outputs.file(outputFile) doFirst { - def f = outputFile.get().asFile - f.parentFile.mkdirs() - standardOutput = new FileOutputStream(f) + args = [outputFile.get().asFile.absolutePath] } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java new file mode 100644 index 00000000000..1324b17b361 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java @@ -0,0 +1,86 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.doc; + +import java.io.IOException; +import java.io.PrintStream; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; + +import com.github.javaparser.ParserConfiguration; +import com.github.javaparser.StaticJavaParser; +import org.jspecify.annotations.Nullable; + +/** + * Base class for the documentation generators of KeY's taclet language constructs, e.g., for the + * variable conditions ({@link VarcondDoc}) and the proof script commands ({@link ScriptDoc}). It + * provides the shared handling of the output target and the post-processing of javadoc text. + * + * @author Alexander Weigl + * @version 1 (23.08.26) + */ +public abstract class AbstractDocGenerator { + + /// Runs this generator. If a command line argument is given, the markdown output is written + /// to that file; otherwise it is printed to stdout. + /// + /// @param args an optional single argument with the path of the output file + /// @throws IOException if the output file cannot be written + protected void run(@Nullable String... args) throws IOException { + var config = new ParserConfiguration(); + config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_21); + StaticJavaParser.setConfiguration(config); + + if (args != null && args.length > 0) { + Path file = Path.of(args[0]); + if (file.getParent() != null) { + Files.createDirectories(file.getParent()); + } + try (var out = + new PrintStream(Files.newOutputStream(file), false, StandardCharsets.UTF_8)) { + generateDocumentation(out); + } + } else { + generateDocumentation(System.out); + } + } + + /// Writes the documentation of this generator in markdown format. + protected abstract void generateDocumentation(PrintStream out); + + /// Converts a javadoc comment into markdown by replacing common HTML tags and inline tags + /// with their markdown equivalents. + /// + /// @param it the javadoc comment, may be null + /// @return the comment as markdown + protected static String cleanJavadoc(@Nullable String it) { + if (it == null) { + it = ""; + } + return it.replace("", "`") + .replace("
      ", "\n") + .replace("
    ", "\n") + .replace("
      ", "\n") + .replace("
    • ", "* ") + .replace("
      • ", "") + .replace("{@link", "`") + .replace("}", "`") + .replace("", "`") + .replace("      ", "`") + .replace("", "`") + .replace("", "**") + .replace("", "**"); + } + + /// Indents each line of the given text by the given prefix. + /// + /// @param spaces the indentation prefix + /// @param it the text to indent + /// @return the indented text + protected static String indent(String spaces, String it) { + return spaces + it.replace("\n", "\n" + spaces); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java index 529a3eb1d8c..f238d6e65fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java @@ -4,6 +4,7 @@ * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.doc; +import java.io.PrintStream; import java.util.ArrayList; import java.util.Comparator; @@ -11,18 +12,28 @@ import de.uka.ilkd.key.scripts.ProofScriptEngine; /** + * Generates the markdown documentation of all proof script commands (loaded via + * {@link ProofScriptEngine#loadCommands()}), based on their self-documentation. * * @author Alexander Weigl * @version 1 (23.08.26) */ -public class ScriptDoc { - public static void main(String[] args) { +public class ScriptDoc extends AbstractDocGenerator { + + public static void main(String[] args) throws Exception { + new ScriptDoc().run(args); + } + + @Override + protected void generateDocumentation(PrintStream out) { var commands = new ArrayList<>(ProofScriptEngine.loadCommands().values()); commands.sort(Comparator.comparing(ProofScriptCommand::getName)); for (var command : commands) { - System.out.println(command.getDocumentation()); - System.out.println("\n\n\n"); + out.println(); + out.println(); + out.format("### `%s`\n\n", command.getName()); + out.println(cleanJavadoc(command.getDocumentation())); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java index 9ae3cd9b717..5441178c33e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java @@ -4,6 +4,7 @@ * SPDX-License-Identifier: GPL-2.0-or-later */ package de.uka.ilkd.key.doc; +import java.io.PrintStream; import java.util.Arrays; import java.util.Comparator; import java.util.function.Function; @@ -13,24 +14,24 @@ import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommandInfo; import de.uka.ilkd.key.nparser.varexp.TacletBuilderManipulators; -import com.github.javaparser.ParserConfiguration; -import com.github.javaparser.StaticJavaParser; import com.github.therapi.runtimejavadoc.CommentFormatter; import com.google.common.collect.Streams; -import org.jspecify.annotations.Nullable; /** + * Generates the markdown documentation of all variable conditions (varconds) registered in + * {@link TacletBuilderManipulators}, extracted from the javadocs of the implementing classes. * * @author Alexander Weigl * @version 1 (23.08.26) */ -public class VarcondDoc { - // region - public static void main(String[] args) { - var config = new ParserConfiguration(); - config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_21); - StaticJavaParser.setConfiguration(config); +public class VarcondDoc extends AbstractDocGenerator { + public static void main(String[] args) throws Exception { + new VarcondDoc().run(args); + } + + @Override + protected void generateDocumentation(PrintStream out) { Function normalizeCmdName = (String it) -> it.startsWith("\\") ? it.replace("\\\\", "\\") : "\\" + it; Function getTriggerName = TacletBuilderCommandInfo::name; @@ -46,16 +47,16 @@ public static void main(String[] args) { for (var name : conds) { var cmds = g.get(name); - System.out.println(); - System.out.println(); - System.out.format("### `%s`\n\n", name); + out.println(); + out.println(); + out.format("### `%s`\n\n", name); cmds.sort(reversed); final var generalDocumentation = cmds.getFirst().getGeneralDocumentation(); - System.out.println( + out.println( cleanJavadoc(new CommentFormatter().format(generalDocumentation.getComment()))); - System.out.format("\n**Signatures**\n\n"); + out.format("\n**Signatures**\n\n"); for (TacletBuilderCommandInfo cmd : cmds) { final var arguments = Streams.zip( @@ -63,46 +64,23 @@ public static void main(String[] args) { Arrays.stream(cmd.argumentTypes()).map(Enum::toString), "%s: %s"::formatted) .collect(Collectors.joining(", ")); - System.out.printf("* `%s(%s)`\n", name, arguments); + out.printf("* `%s(%s)`\n", name, arguments); if (cmd.isNegationSupported()) { - System.out.printf("* `\\not%s(%s)`\n", name, arguments); + out.printf("* `\\not%s(%s)`\n", name, arguments); } - System.out.println(); + out.println(); final var argumentInformation = cmd.getArgumentInformation(); - System.out.println( + out.println( indent(" ", cleanJavadoc(argumentInformation.getComment().toString()))); - System.out.println(); + out.println(); argumentInformation.getParams().stream() .map(tag -> " * `%s` %s".formatted(tag.getName(), tag.getComment())) - .forEach(System.out::println); - System.out.println(); + .forEach(out::println); + out.println(); } } } - - private static String indent(String spaces, String it) { - return spaces + it.replace("\n", "\n" + spaces); - } - - private static String cleanJavadoc(@Nullable String it) { - if (it == null) - it = ""; - return it.replace("", "`") - .replace("
        ", "\n") - .replace("
      ", "\n") - .replace("
        ", "\n") - .replace("
      • ", "* ") - .replace("
        • ", "") - .replace("{@link", "`") - .replace("}", "`") - .replace("", "`") - .replace("        ", "`") - .replace("", "`") - .replace("", "**") - .replace("", "**"); - } - // endregion } From 9ec0b2908448b61fc1d6b73dece67b4c571befb3 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 10 Oct 2026 15:33:36 +0200 Subject: [PATCH 09/11] key.core: add JSON dumps to the documentation generators The generators now also emit a structured JSON dump next to the markdown file (varconds.json, script-commands.json), containing the same information in a machine-readable form: names, categories, deprecation flags, descriptions, signatures with negation support, and arguments with kind, type, position and description. The shared base class AbstractDocGenerator gains a generateJsonData() hook; the new dependency-free JsonWriter serializes the data. The nightly workflow's packaging step picks the JSON files up unchanged. --- key.core/build.gradle | 2 + .../ilkd/key/doc/AbstractDocGenerator.java | 27 ++++- .../java/de/uka/ilkd/key/doc/JsonWriter.java | 108 ++++++++++++++++++ .../java/de/uka/ilkd/key/doc/ScriptDoc.java | 49 +++++++- .../java/de/uka/ilkd/key/doc/VarcondDoc.java | 91 ++++++++++++--- 5 files changed, 253 insertions(+), 24 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java diff --git a/key.core/build.gradle b/key.core/build.gradle index 1fce543f748..e6c10dc0078 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -79,6 +79,7 @@ tasks.register('generateVarcondDoc', JavaExec) { mainClass = 'de.uka.ilkd.key.doc.VarcondDoc' def outputFile = layout.buildDirectory.file("docs/keydocs/varconds.md") outputs.file(outputFile) + outputs.file(layout.buildDirectory.file("docs/keydocs/varconds.json")) doFirst { args = [outputFile.get().asFile.absolutePath] } @@ -93,6 +94,7 @@ tasks.register('generateScriptDoc', JavaExec) { mainClass = 'de.uka.ilkd.key.doc.ScriptDoc' def outputFile = layout.buildDirectory.file("docs/keydocs/script-commands.md") outputs.file(outputFile) + outputs.file(layout.buildDirectory.file("docs/keydocs/script-commands.json")) doFirst { args = [outputFile.get().asFile.absolutePath] } diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java index 1324b17b361..f623c8d6c42 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java @@ -25,7 +25,8 @@ public abstract class AbstractDocGenerator { /// Runs this generator. If a command line argument is given, the markdown output is written - /// to that file; otherwise it is printed to stdout. + /// to that file together with a JSON dump ([#generateJsonData()]) next to it; otherwise the + /// markdown is printed to stdout. /// /// @param args an optional single argument with the path of the output file /// @throws IOException if the output file cannot be written @@ -35,14 +36,21 @@ protected void run(@Nullable String... args) throws IOException { StaticJavaParser.setConfiguration(config); if (args != null && args.length > 0) { - Path file = Path.of(args[0]); - if (file.getParent() != null) { - Files.createDirectories(file.getParent()); + Path mdFile = Path.of(args[0]); + if (mdFile.getParent() != null) { + Files.createDirectories(mdFile.getParent()); } try (var out = - new PrintStream(Files.newOutputStream(file), false, StandardCharsets.UTF_8)) { + new PrintStream(Files.newOutputStream(mdFile), false, StandardCharsets.UTF_8)) { generateDocumentation(out); } + Object data = generateJsonData(); + if (data != null) { + Path jsonFile = + mdFile.resolveSibling(mdFile.getFileName().toString().replaceFirst("\\.md$", + "") + ".json"); + Files.writeString(jsonFile, JsonWriter.toJson(data) + "\n"); + } } else { generateDocumentation(System.out); } @@ -51,6 +59,15 @@ protected void run(@Nullable String... args) throws IOException { /// Writes the documentation of this generator in markdown format. protected abstract void generateDocumentation(PrintStream out); + /// Returns the documentation data of this generator in a structured form, which is serialized + /// into a JSON dump next to the markdown file. Returns `null` if this generator does not + /// support a JSON dump. + /// + /// @return the structured documentation data, or `null` + protected @Nullable Object generateJsonData() { + return null; + } + /// Converts a javadoc comment into markdown by replacing common HTML tags and inline tags /// with their markdown equivalents. /// diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java b/key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java new file mode 100644 index 00000000000..d550410f428 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java @@ -0,0 +1,108 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.doc; + +import java.util.Map; + +import org.jspecify.annotations.Nullable; + +/** + * A minimal, dependency-free JSON serializer supporting the data structures used by the + * documentation generators: {@link Map}s, {@link Iterable}s, strings, numbers, booleans, and + * {@code null}. Other objects are serialized via their {@link Object#toString()}. + * + * @author Alexander Weigl + * @version 1 (10.10.26) + */ +public final class JsonWriter { + + private JsonWriter() { + } + + /** + * Serializes the given value into a pretty-printed JSON string. + * + * @param value the value to serialize + * @return the JSON representation of the value + */ + public static String toJson(@Nullable Object value) { + var sb = new StringBuilder(); + write(sb, value, 0); + return sb.toString(); + } + + private static void write(StringBuilder sb, @Nullable Object value, int depth) { + switch (value) { + case null -> sb.append("null"); + case String s -> writeString(sb, s); + case Boolean b -> sb.append(b); + case Number n -> sb.append(n); + case Map map -> writeObject(sb, map, depth); + case Iterable iterable -> writeArray(sb, iterable, depth); + default -> writeString(sb, value.toString()); + } + } + + private static void writeObject(StringBuilder sb, Map map, int depth) { + sb.append("{\n"); + var it = map.entrySet().iterator(); + while (it.hasNext()) { + var entry = it.next(); + indent(sb, depth + 1); + writeString(sb, String.valueOf(entry.getKey())); + sb.append(": "); + write(sb, entry.getValue(), depth + 1); + if (it.hasNext()) { + sb.append(','); + } + sb.append('\n'); + } + indent(sb, depth); + sb.append('}'); + } + + private static void writeArray(StringBuilder sb, Iterable iterable, int depth) { + sb.append("[\n"); + var it = iterable.iterator(); + while (it.hasNext()) { + indent(sb, depth + 1); + write(sb, it.next(), depth + 1); + if (it.hasNext()) { + sb.append(','); + } + sb.append('\n'); + } + indent(sb, depth); + sb.append(']'); + } + + private static void writeString(StringBuilder sb, String s) { + sb.append('"'); + for (var i = 0; i < s.length(); i++) { + char c = s.charAt(i); + switch (c) { + case '"' -> sb.append("\\\""); + case '\\' -> sb.append("\\\\"); + case '\n' -> sb.append("\\n"); + case '\r' -> sb.append("\\r"); + case '\t' -> sb.append("\\t"); + case '\b' -> sb.append("\\b"); + case '\f' -> sb.append("\\f"); + default -> { + if (c < 0x20) { + sb.append("\\u%04x".formatted((int) c)); + } else { + sb.append(c); + } + } + } + } + sb.append('"'); + } + + private static void indent(StringBuilder sb, int depth) { + sb.append(" ".repeat(depth)); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java index f238d6e65fe..34202d41c8e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java @@ -7,9 +7,13 @@ import java.io.PrintStream; import java.util.ArrayList; import java.util.Comparator; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; import de.uka.ilkd.key.scripts.ProofScriptCommand; import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.meta.ProofScriptArgument; /** * Generates the markdown documentation of all proof script commands (loaded via @@ -26,14 +30,51 @@ public static void main(String[] args) throws Exception { @Override protected void generateDocumentation(PrintStream out) { - var commands = new ArrayList<>(ProofScriptEngine.loadCommands().values()); - commands.sort(Comparator.comparing(ProofScriptCommand::getName)); - - for (var command : commands) { + for (var command : sortedCommands()) { out.println(); out.println(); out.format("### `%s`\n\n", command.getName()); out.println(cleanJavadoc(command.getDocumentation())); } } + + @Override + protected Object generateJsonData() { + var commands = new ArrayList>(); + for (var command : sortedCommands()) { + var data = new LinkedHashMap(); + data.put("name", command.getName()); + data.put("category", command.getCategory()); + data.put("deprecated", command.getClass().isAnnotationPresent(Deprecated.class)); + data.put("documentation", cleanJavadoc(command.getDocumentation())); + + var arguments = new ArrayList>(); + for (ProofScriptArgument meta : command.getArguments()) { + var argument = new LinkedHashMap(); + argument.put("name", meta.getName()); + argument.put("type", meta.getType().getSimpleName()); + argument.put("kind", + meta.isFlag() ? "flag" : meta.isOption() ? "option" : "positional"); + argument.put("required", meta.isRequired()); + if (meta.isPositional()) { + argument.put("position", meta.getArgumentPosition()); + } + if (meta.isPositionalVarArgs() || meta.isOptionalVarArgs()) { + argument.put("varargs", true); + } + argument.put("description", meta.getDocumentation()); + arguments.add(argument); + } + data.put("arguments", arguments); + commands.add(data); + } + return Map.of("commands", commands); + } + + /// Returns all loaded proof script commands sorted by their name. + private List sortedCommands() { + var commands = new ArrayList<>(ProofScriptEngine.loadCommands().values()); + commands.sort(Comparator.comparing(ProofScriptCommand::getName)); + return commands; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java index 5441178c33e..3c44123d589 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java @@ -5,8 +5,12 @@ package de.uka.ilkd.key.doc; import java.io.PrintStream; +import java.util.ArrayList; import java.util.Arrays; import java.util.Comparator; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; import java.util.function.Function; import java.util.stream.Collectors; @@ -32,25 +36,13 @@ public static void main(String[] args) throws Exception { @Override protected void generateDocumentation(PrintStream out) { - Function normalizeCmdName = - (String it) -> it.startsWith("\\") ? it.replace("\\\\", "\\") : "\\" + it; - Function getTriggerName = TacletBuilderCommandInfo::name; - - var g = TacletBuilderManipulators.getConditionBuilders().stream() - .map(TacletBuilderCommand::getInformation) - .collect(Collectors.groupingBy(getTriggerName.andThen(normalizeCmdName))); - Comparator reversed = - Comparator.comparing((TacletBuilderCommandInfo it) -> it.argumentTypes().length) - .reversed(); + for (var entry : collectVarconds().entrySet()) { + String name = entry.getKey(); + List cmds = entry.getValue(); - var conds = g.keySet().stream().sorted().toList(); - - for (var name : conds) { - var cmds = g.get(name); out.println(); out.println(); out.format("### `%s`\n\n", name); - cmds.sort(reversed); final var generalDocumentation = cmds.getFirst().getGeneralDocumentation(); out.println( @@ -83,4 +75,73 @@ protected void generateDocumentation(PrintStream out) { } } } + + @Override + protected Object generateJsonData() { + var varconds = new ArrayList>(); + for (var entry : collectVarconds().entrySet()) { + String name = entry.getKey(); + List cmds = entry.getValue(); + + var varcond = new LinkedHashMap(); + varcond.put("name", name); + final var generalDocumentation = cmds.getFirst().getGeneralDocumentation(); + varcond.put("description", + cleanJavadoc(new CommentFormatter().format(generalDocumentation.getComment()))); + + var signatures = new ArrayList>(); + for (TacletBuilderCommandInfo cmd : cmds) { + final var argumentInformation = cmd.getArgumentInformation(); + var params = argumentInformation.getParams(); + + var signature = new LinkedHashMap(); + signature.put("negated", cmd.isNegationSupported()); + signature.put("description", + cleanJavadoc(argumentInformation.getComment().toString())); + + var arguments = new ArrayList>(); + for (var i = 0; i < cmd.argumentTypes().length; i++) { + var argument = new LinkedHashMap(); + argument.put("name", cmd.argNames()[i]); + argument.put("type", cmd.argumentTypes()[i].toString()); + if (i < params.size()) { + final var comment = params.get(i).getComment(); + argument.put("description", + cleanJavadoc(comment == null ? null : comment.toString())); + } + arguments.add(argument); + } + signature.put("arguments", arguments); + signatures.add(signature); + } + varcond.put("signatures", signatures); + varconds.add(varcond); + } + return Map.of("varconds", varconds); + } + + /// Collects all registered variable conditions, grouped and sorted by their trigger name; + /// within a group, the signatures are sorted by the number of declared argument types + /// (descending). + private LinkedHashMap> collectVarconds() { + Function normalizeCmdName = + (String it) -> it.startsWith("\\") ? it.replace("\\\\", "\\") : "\\" + it; + Function getTriggerName = TacletBuilderCommandInfo::name; + + var grouped = TacletBuilderManipulators.getConditionBuilders().stream() + .map(TacletBuilderCommand::getInformation) + .collect(Collectors.groupingBy(getTriggerName.andThen(normalizeCmdName))); + Comparator reversed = + Comparator.comparing((TacletBuilderCommandInfo it) -> it.argumentTypes().length) + .reversed(); + + var result = new LinkedHashMap>(); + grouped.keySet().stream().sorted().forEach( + name -> { + var cmds = grouped.get(name); + cmds.sort(reversed); + result.put(name, cmds); + }); + return result; + } } From d10d52980d6e124bb7adb0fbdd8ce7b8581d4678 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 11 Oct 2026 16:19:02 +0200 Subject: [PATCH 10/11] fix reviewer comment --- .../uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index c3c5691835b..753d2261880 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -262,7 +262,7 @@ public VariableCondition build(Object[] arguments, List parameters, } }; public static final AbstractConditionBuilder ENUM_TYPE = - new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV, SV, SV); + new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV); public static final AbstractConditionBuilder CONTAINS_ASSIGNMENT = new ConstructorBasedBuilder("containsAssignment", ContainsAssignmentCondition.class, SV); public static final AbstractConditionBuilder FIELD_TYPE = From c94ff2d8abdc1aac88475260b07bce222d24502e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 11 Oct 2026 16:46:15 +0200 Subject: [PATCH 11/11] clean up AI --- .github/workflows/nightlydeploy.yml | 37 ++--- build.gradle | 4 - key.core/build.gradle | 18 ++- .../ilkd/key/doc/AbstractDocGenerator.java | 149 +++++++++++++++--- .../java/de/uka/ilkd/key/doc/JsonWriter.java | 108 ------------- .../java/de/uka/ilkd/key/doc/ScriptDoc.java | 2 +- .../java/de/uka/ilkd/key/doc/VarcondDoc.java | 2 +- 7 files changed, 149 insertions(+), 171 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index a8484f91bb5..e6b76fbbb25 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -9,8 +9,11 @@ permissions: contents: write id-token: write +# The documentation generation for varconds and proof script commands +# extracts `///` markdown javadocs via therapi, which requires JDK 23+. +# `--release=21` is still set! env: - JAVA_VERSION: 21 + JAVA_VERSION: 25 jobs: @@ -29,7 +32,7 @@ jobs: uses: gradle/actions/setup-gradle@v6 - name: Build with Gradle - run: ./gradlew --parallel assemble javadoc alldoc + run: ./gradlew --parallel assemble javadoc alldoc :key.core:generateVarcondDoc :key.core:generateScriptDoc - name: Upload ShadowJars (fat and slim) uses: actions/upload-artifact@v7 @@ -40,6 +43,14 @@ jobs: path: "*/build/libs/*-exe.jar" retention-days: 1 + - name: Upload varcond and proof script documentation + uses: actions/upload-artifact@v7 + with: + name: varcond-script-docs + path: "key.core/build/docs/keydocs/*" + retention-days: 30 + compression-level: '9' + - name: Package run: tar cvf key-javadoc.tar.xz build/docs/javadoc @@ -80,25 +91,3 @@ jobs: ORG_GRADLE_PROJECT_signingInMemoryKeyPassword: ${{secrets.GPG_PASSPHRASE}} ORG_GRADLE_PROJECT_mavenCentralUsername: ${{ secrets.SONATYPE_USERNAME }} ORG_GRADLE_PROJECT_mavenCentralPassword: ${{ secrets.SONATYPE_PASSWORD }} - - # The documentation generation for varconds and proof script commands - # extracts `///` markdown javadocs via therapi, which requires JDK 23+. - - name: Set up JDK 25 (documentation generation) - uses: actions/setup-java@v6.0.1 - with: - java-version: '25' - distribution: 'temurin' - cache: 'gradle' - - - name: Generate varcond and proof script documentation - run: ./gradlew --parallel :key.core:generateVarcondDoc :key.core:generateScriptDoc - - - name: Package varcond and proof script documentation - run: zip -j key-varcond-script-docs.zip key.core/build/docs/keydocs/* - - - name: Upload varcond and proof script documentation - uses: actions/upload-artifact@v7 - with: - name: varcond-script-docs - path: "key-varcond-script-docs.zip" - retention-days: 30 diff --git a/build.gradle b/build.gradle index 5d3edfa1a90..c89c5127e6a 100644 --- a/build.gradle +++ b/build.gradle @@ -83,10 +83,6 @@ subprojects { implementation(libs.slf4j.api) testImplementation(libs.logback.classic) - - // Therapi runtime javadoc - annotationProcessor 'com.github.therapi:therapi-runtime-javadoc-scribe:0.13.0' - implementation 'com.github.therapi:therapi-runtime-javadoc:0.13.0' compileOnly(libs.jspecify) testCompileOnly(libs.jspecify) compileOnly(libs.checkerframework.qual) diff --git a/key.core/build.gradle b/key.core/build.gradle index e6c10dc0078..f12b7330bac 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -77,11 +77,12 @@ tasks.register('generateVarcondDoc', JavaExec) { description = 'Generates the markdown documentation of all variable conditions (varconds).' classpath = sourceSets.main.runtimeClasspath mainClass = 'de.uka.ilkd.key.doc.VarcondDoc' - def outputFile = layout.buildDirectory.file("docs/keydocs/varconds.md") - outputs.file(outputFile) - outputs.file(layout.buildDirectory.file("docs/keydocs/varconds.json")) + def mdFile = layout.buildDirectory.file("docs/keydocs/varconds.md") + def jsonFile = layout.buildDirectory.file("docs/keydocs/varconds.json") + outputs.file(mdFile) + outputs.file(jsonFile) doFirst { - args = [outputFile.get().asFile.absolutePath] + args = [mdFile.get().asFile.absolutePath, jsonFile.get().asFile.absolutePath ] } } @@ -92,11 +93,12 @@ tasks.register('generateScriptDoc', JavaExec) { description = 'Generates the markdown documentation of all proof script commands.' classpath = sourceSets.main.runtimeClasspath mainClass = 'de.uka.ilkd.key.doc.ScriptDoc' - def outputFile = layout.buildDirectory.file("docs/keydocs/script-commands.md") - outputs.file(outputFile) - outputs.file(layout.buildDirectory.file("docs/keydocs/script-commands.json")) + def mdFile = layout.buildDirectory.file("docs/keydocs/script-commands.md") + def jsonFile = layout.buildDirectory.file("docs/keydocs/script-commands.json") + outputs.file(mdFile) + outputs.file(jsonFile) doFirst { - args = [outputFile.get().asFile.absolutePath] + args = [mdFile.get().asFile.absolutePath, jsonFile.get().asFile.absolutePath ] } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java index f623c8d6c42..f73fbbbcb1b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java @@ -6,12 +6,12 @@ import java.io.IOException; import java.io.PrintStream; -import java.nio.charset.StandardCharsets; +import java.io.PrintWriter; import java.nio.file.Files; import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Map; -import com.github.javaparser.ParserConfiguration; -import com.github.javaparser.StaticJavaParser; import org.jspecify.annotations.Nullable; /** @@ -28,31 +28,30 @@ public abstract class AbstractDocGenerator { /// to that file together with a JSON dump ([#generateJsonData()]) next to it; otherwise the /// markdown is printed to stdout. /// - /// @param args an optional single argument with the path of the output file + /// @param mdFile an optional single argument with the path of the output file + /// @param jsonFile /// @throws IOException if the output file cannot be written - protected void run(@Nullable String... args) throws IOException { - var config = new ParserConfiguration(); - config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_21); - StaticJavaParser.setConfiguration(config); - - if (args != null && args.length > 0) { - Path mdFile = Path.of(args[0]); - if (mdFile.getParent() != null) { - Files.createDirectories(mdFile.getParent()); - } - try (var out = - new PrintStream(Files.newOutputStream(mdFile), false, StandardCharsets.UTF_8)) { - generateDocumentation(out); + protected void run(String mdFile, String jsonFile) throws IOException { + Path mdPath = Path.of(mdFile); + if (mdPath.getParent() != null) { + Files.createDirectories(mdPath.getParent()); + } + + try (var out = new PrintStream(Files.newOutputStream(mdPath), false)) { + generateDocumentation(out); + } + + + Object data = generateJsonData(); + + if (data != null) { + Path jsonPath = Paths.get(jsonFile); + if (jsonPath.getParent() != null) { + Files.createDirectories(jsonPath.getParent()); } - Object data = generateJsonData(); - if (data != null) { - Path jsonFile = - mdFile.resolveSibling(mdFile.getFileName().toString().replaceFirst("\\.md$", - "") + ".json"); - Files.writeString(jsonFile, JsonWriter.toJson(data) + "\n"); + try (var out = new PrintWriter(Files.newOutputStream(jsonPath), false)) { + JsonWriter.toJson(data, out); } - } else { - generateDocumentation(System.out); } } @@ -101,3 +100,103 @@ protected static String indent(String spaces, String it) { return spaces + it.replace("\n", "\n" + spaces); } } + + +/** + * A minimal, dependency-free JSON serializer supporting the data structures used by the + * documentation generators: {@link Map}s, {@link Iterable}s, strings, numbers, booleans, and + * {@code null}. Other objects are serialized via their {@link Object#toString()}. + * + * @author Alexander Weigl + * @version 1 (10.10.26) + */ +final class JsonWriter { + + private JsonWriter() { + } + + /** + * Serializes the given value into a pretty-printed JSON string. + * + * @param value the value to serialize + * @param out target to write into + */ + public static void toJson(@Nullable Object value, PrintWriter out) { + write(out, value, 0); + } + + private static void write(PrintWriter sb, @Nullable Object value, int depth) { + switch (value) { + case null -> sb.append("null"); + case String s -> writeString(sb, s); + case Boolean b -> sb.print(b); + case Number n -> sb.print(n); + case Map map -> writeObject(sb, map, depth); + case Iterable iterable -> writeArray(sb, iterable, depth); + default -> writeString(sb, value.toString()); + } + } + + private static void writeObject(PrintWriter sb, Map map, int depth) { + sb.append("{\n"); + var it = map.entrySet().iterator(); + while (it.hasNext()) { + var entry = it.next(); + indent(sb, depth + 1); + writeString(sb, String.valueOf(entry.getKey())); + sb.append(": "); + write(sb, entry.getValue(), depth + 1); + if (it.hasNext()) { + sb.append(','); + } + sb.append('\n'); + } + indent(sb, depth); + sb.append('}'); + } + + private static void writeArray(PrintWriter sb, Iterable iterable, int depth) { + sb.append("[\n"); + var it = iterable.iterator(); + while (it.hasNext()) { + indent(sb, depth + 1); + write(sb, it.next(), depth + 1); + if (it.hasNext()) { + sb.append(','); + } + sb.append('\n'); + } + indent(sb, depth); + sb.append(']'); + } + + private static void writeString(PrintWriter sb, String s) { + sb.append('"'); + for (var i = 0; i < s.length(); i++) { + char c = s.charAt(i); + switch (c) { + case '"' -> sb.append("\\\""); + case '\\' -> sb.append("\\\\"); + case '\n' -> sb.append("\\n"); + case '\r' -> sb.append("\\r"); + case '\t' -> sb.append("\\t"); + case '\b' -> sb.append("\\b"); + case '\f' -> sb.append("\\f"); + default -> { + if (c < 0x20) { + sb.append("\\u%04x".formatted((int) c)); + } else { + sb.append(c); + } + } + } + } + sb.append('"'); + } + + private static void indent(PrintWriter sb, int depth) { + sb.append(" ".repeat(depth)); + } +} +\newLocalVars(varDeclsSV: VARIABLE, updateBeforeSV: VARIABLE, updateFrameSV: VARIABLE, bodySV: VARIABLE) + diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java b/key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java deleted file mode 100644 index d550410f428..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/JsonWriter.java +++ /dev/null @@ -1,108 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2, - * or (at your option) any later version. - * SPDX-License-Identifier: GPL-2.0-or-later */ -package de.uka.ilkd.key.doc; - -import java.util.Map; - -import org.jspecify.annotations.Nullable; - -/** - * A minimal, dependency-free JSON serializer supporting the data structures used by the - * documentation generators: {@link Map}s, {@link Iterable}s, strings, numbers, booleans, and - * {@code null}. Other objects are serialized via their {@link Object#toString()}. - * - * @author Alexander Weigl - * @version 1 (10.10.26) - */ -public final class JsonWriter { - - private JsonWriter() { - } - - /** - * Serializes the given value into a pretty-printed JSON string. - * - * @param value the value to serialize - * @return the JSON representation of the value - */ - public static String toJson(@Nullable Object value) { - var sb = new StringBuilder(); - write(sb, value, 0); - return sb.toString(); - } - - private static void write(StringBuilder sb, @Nullable Object value, int depth) { - switch (value) { - case null -> sb.append("null"); - case String s -> writeString(sb, s); - case Boolean b -> sb.append(b); - case Number n -> sb.append(n); - case Map map -> writeObject(sb, map, depth); - case Iterable iterable -> writeArray(sb, iterable, depth); - default -> writeString(sb, value.toString()); - } - } - - private static void writeObject(StringBuilder sb, Map map, int depth) { - sb.append("{\n"); - var it = map.entrySet().iterator(); - while (it.hasNext()) { - var entry = it.next(); - indent(sb, depth + 1); - writeString(sb, String.valueOf(entry.getKey())); - sb.append(": "); - write(sb, entry.getValue(), depth + 1); - if (it.hasNext()) { - sb.append(','); - } - sb.append('\n'); - } - indent(sb, depth); - sb.append('}'); - } - - private static void writeArray(StringBuilder sb, Iterable iterable, int depth) { - sb.append("[\n"); - var it = iterable.iterator(); - while (it.hasNext()) { - indent(sb, depth + 1); - write(sb, it.next(), depth + 1); - if (it.hasNext()) { - sb.append(','); - } - sb.append('\n'); - } - indent(sb, depth); - sb.append(']'); - } - - private static void writeString(StringBuilder sb, String s) { - sb.append('"'); - for (var i = 0; i < s.length(); i++) { - char c = s.charAt(i); - switch (c) { - case '"' -> sb.append("\\\""); - case '\\' -> sb.append("\\\\"); - case '\n' -> sb.append("\\n"); - case '\r' -> sb.append("\\r"); - case '\t' -> sb.append("\\t"); - case '\b' -> sb.append("\\b"); - case '\f' -> sb.append("\\f"); - default -> { - if (c < 0x20) { - sb.append("\\u%04x".formatted((int) c)); - } else { - sb.append(c); - } - } - } - } - sb.append('"'); - } - - private static void indent(StringBuilder sb, int depth) { - sb.append(" ".repeat(depth)); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java index 34202d41c8e..69b610f9c25 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java @@ -25,7 +25,7 @@ public class ScriptDoc extends AbstractDocGenerator { public static void main(String[] args) throws Exception { - new ScriptDoc().run(args); + new ScriptDoc().run(args[0], args[1]); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java index 3c44123d589..46f1660cd23 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java +++ b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java @@ -31,7 +31,7 @@ public class VarcondDoc extends AbstractDocGenerator { public static void main(String[] args) throws Exception { - new VarcondDoc().run(args); + new VarcondDoc().run(args[0], args[1]); } @Override