Profile-dependent option panel in loading dialog

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java

@@ -325,4 +325,9 @@ public static boolean isTruthValueEvaluationEnabled(Profile profile) {
             return false;
         }
     }
+
+    @Override
+    public String displayName() {
+        return NAME;
+    }
 }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java

@@ -27,7 +27,6 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.OneStepSimplifier;
 import de.uka.ilkd.key.rule.Taclet;
-import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile;
@@ -817,9 +816,7 @@ protected ImmutableList<TermLabelConfiguration> computeTermLabelConfiguration()
                 ? new ProofSettings(sourceInitConfig.getSettings())
                 : null;
         initConfig.setSettings(clonedSettings);
-        initConfig.setTaclet2Builder(
-            (HashMap<Taclet, TacletBuilder<? extends Taclet>>) sourceInitConfig.getTaclet2Builder()
-                    .clone());
+        initConfig.setTaclet2Builder(new HashMap<>(sourceInitConfig.getTaclet2Builder()));
         initConfig.setTaclets(sourceInitConfig.getTaclets());
         // Create new ProofEnvironment and initialize it with values from initial one.
         ProofEnvironment env = new ProofEnvironment(initConfig);

key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java

@@ -15,11 +15,14 @@
 import de.uka.ilkd.key.proof.io.RuleSourceFactory;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
 import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.util.KeYResourceManager;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * @author Alexander Weigl
  * @version 1 (7/27/25)
@@ -97,9 +100,19 @@ public RuleCollection getStandardRules() {
         return wdStandardRules;
     }
 
+    /// {@inheritDoc}
+    ///
+    /// @param additionalProfileOptions a string representing the choice of `wdOperator`
     @Override
-    public void prepareInitConfig(InitConfig baseConfig) {
+    public void prepareInitConfig(InitConfig baseConfig,
+            @Nullable Configuration additionalProfileOptions) {
         var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
         baseConfig.activateChoice(wdChoice);
+
+        if (additionalProfileOptions != null) {
+            var wdOperator =
+                baseConfig.choiceNS().lookup(new Name(additionalProfileOptions.toString()));
+            baseConfig.activateChoice(wdOperator);
+        }
     }
 }

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key

@@ -2,6 +2,51 @@
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
 
+\optionsDecl {
+		/*!
+    Treatment of formulas and terms for welldefinedness checks:
+    */
+    wdOperator: {
+        /*!
+        More intuitive for software developers and along the lines of
+        runtime assertion semantics. Well-Definedness checks will be
+        stricter using this operator, since the order of terms/formulas
+        matters. It is based on McCarthy logic.
+        Cf. "Are the Logical Foundations of Verifying Compiler
+        Prototypes Matching User Expectations?" by Patrice Chalin.
+
+        @choiceDefaultOption
+        */
+        L,
+        /*!
+        Complete and along the lines of classical logic, where the
+        order of terms/formulas is irrelevant. This operator is
+        equivalent to the D-operator, but more efficient.
+        Cf. "Efficient Well-Definedness Checking" by Ádám Darvas,
+        Farhad Mehta, and Arsenii Rudich.
+        */
+        Y,
+        /*!
+        Complete and along the lines of classical logic, where the
+        order of terms/formulas is irrelevant. This operator is not as
+        strict as the L-operator, based on strong Kleene logic. To be
+        used with care, since formulas may blow up exponentially.
+        Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and
+        Jean-Marc Meynadier*/
+        D
+    };
+
+    /*!
+    Welldefinedness checks of JML specifications can be turned on/off.
+    This includes class invariants, operation contracts, model fields
+    as well as JML (annotation) statements as loop invariants and
+    block contracts. The former ones are checked "on-the-fly", i.e.,
+    directly when they are applied in the code while proving an operation
+    contract, since the context is needed.
+    */
+    wdChecks: {off, on};
+}
+
 \transformers {
     \formula wd(any);
     \formula WD(\formula);

key.core/src/main/antlr4/KeYParser.g4

@@ -90,11 +90,11 @@ one_sort_decl
 :
   doc=DOC_COMMENT?
   (
-     GENERIC  sortIds=simple_ident_dots_comma_list
+     GENERIC  sortIds=simple_ident_dots_comma_list_with_docs
         (ONEOF sortOneOf = oneof_sorts)?
         (EXTENDS sortExt = extends_sorts)? SEMI
-    | PROXY  sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI
-    | ABSTRACT? sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)?  SEMI
+    | PROXY  sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)? SEMI
+    | ABSTRACT? sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)?  SEMI
   )
 ;
 
@@ -108,6 +108,13 @@ simple_ident_dots_comma_list
   simple_ident_dots (COMMA simple_ident_dots)*
 ;
 
+simple_ident_dots_comma_list_with_docs
+:
+    simple_ident_dots_with_docs (COMMA simple_ident_dots_with_docs)*
+;
+
+simple_ident_dots_with_docs: DOC_COMMENT? simple_ident_dots;
+
 
 extends_sorts
 :
@@ -132,7 +139,7 @@ prog_var_decls
     LBRACE
     (
         kjt = keyjavatype
-        var_names = simple_ident_comma_list
+        var_names = simple_ident_comma_list_with_docs
         SEMI
     )*
     RBRACE
@@ -154,6 +161,10 @@ simple_ident_comma_list
     id = simple_ident (COMMA id = simple_ident )*
 ;
 
+simple_ident_comma_list_with_docs
+:
+    id+=simple_ident_with_doc (COMMA id+=simple_ident_with_doc)*
+;
 
 schema_var_decls :
     SCHEMAVARIABLES LBRACE
@@ -250,6 +261,7 @@ datatype_decl:
 ;
 
 datatype_constructor:
+  doc=DOC_COMMENT?
   name=simple_ident
   (
     LPAREN
@@ -321,7 +333,12 @@ where_to_bind:
 
 ruleset_decls
 :
-  HEURISTICSDECL LBRACE  (doc+=DOC_COMMENT? id+=simple_ident SEMI)* RBRACE
+  HEURISTICSDECL LBRACE  (id+=simple_ident_with_doc SEMI)* RBRACE
+;
+
+simple_ident_with_doc
+:
+    doc=DOC_COMMENT? id=simple_ident
 ;
 
 sortId

key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java

@@ -157,7 +157,7 @@ public TermLabelVisibilityManagerListener[] getTermLabelVisibilityManagerListene
 
     /**
      * Fires the event
-     * {@link TermLabelVisibilityManagerListener#visibleLabelsChanged( TermLabelVisibilityManagerEvent)}
+     * {@link TermLabelVisibilityManagerListener#visibleLabelsChanged(TermLabelVisibilityManagerEvent)}
      * to all listeners.
      *
      * @param e The event object.

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

@@ -762,7 +762,7 @@ public DLEmbeddedExpression convert(EscapeExpression e) {
                     sortName, e.getStartPosition()));
             }
 
-            var doc = sort.getDocumentation();
+            var doc = namespaceSet.docs().find(sort);
 
             if (doc == null) {
                 throw new ConvertException(

key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.ldt;
 
+import java.util.Objects;
+
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.settings.ProofSettings;
 
@@ -51,8 +53,8 @@ public static boolean isFinalEnabled(@NonNull InitConfig initConfig) {
      * @return true if final fields are treated as immutable
      */
     public static boolean isFinalEnabled(@NonNull ProofSettings settings) {
-        return settings.getChoiceSettings().getDefaultChoices().get(SETTING)
-                .equals(IMMUTABLE_OPTION);
+        return Objects.equals(settings.getChoiceSettings().getDefaultChoices().get(SETTING),
+            IMMUTABLE_OPTION);
     }
 
     /**

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

@@ -0,0 +1,69 @@
+/* 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.logic;
+
+import java.util.Map;
+import java.util.TreeMap;
+
+import org.key_project.logic.HasDocumentation;
+
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+@NullMarked
+public class DocSpace {
+    private @Nullable DocSpace parent;
+    private final Map<String, String> documentation = new TreeMap<>();
+
+    public DocSpace() {}
+
+    public DocSpace(Map<String, String> documentation) {
+        this.documentation.putAll(documentation);
+    }
+
+    public DocSpace(DocSpace parent) {
+        this.parent = parent;
+    }
+
+    public DocSpace(@Nullable DocSpace parent, Map<String, String> documentation) {
+        this(documentation);
+        this.parent = parent;
+    }
+
+    public @Nullable String find(String key) {
+        var value = documentation.get(key);
+        if (value != null)
+            return value;
+        if (parent != null)
+            return parent.find(key);
+        return null;
+    }
+
+    public @Nullable String find(HasDocumentation entity) {
+        var doc = entity.getDocumentation();
+        if (doc != null) {
+            return doc;
+        }
+        return find(entity.getDocumentationKey());
+    }
+
+    public void add(DocSpace space) {
+        this.documentation.putAll(space.documentation);
+    }
+
+    public @Nullable DocSpace parent() {
+        return parent;
+    }
+
+    public void describe(HasDocumentation entity, @Nullable String doc) {
+        if (doc == null) {
+            return;
+        }
+        documentation.put(entity.getDocumentationKey(), doc);
+    }
+
+    public DocSpace copy() {
+        return new DocSpace(parent, documentation);
+    }
+}