Renovation of the TestCase generation

key.core.testgen/build.gradle

@@ -2,4 +2,5 @@ description "Test Case Generation based on proof attempts."
 
 dependencies {
     implementation project(":key.core")
+    implementation("com.squareup:javapoet:1.13.0")
 }

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java

@@ -0,0 +1,5 @@
+package de.uka.ilkd.key.testgen;
+
+public enum Format {
+    Plain, JUnit4, JUnit5, TestNG,
+}

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java

@@ -21,7 +21,7 @@
 import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.TestGenerationSettings;
+import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.*;
 import de.uka.ilkd.key.smt.lang.SMTSort;
 import de.uka.ilkd.key.smt.model.Model;

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java

@@ -24,16 +24,11 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-public class ProofInfo {
+public record ProofInfo(Proof proof, Services services) {
     private static final Logger LOGGER = LoggerFactory.getLogger(ProofInfo.class);
 
-    private final Proof proof;
-
-    private final Services services;
-
     public ProofInfo(Proof proof) {
-        this.proof = proof;
-        this.services = proof.getServices();
+        this(proof, proof.getServices());
     }
 
     public IProgramMethod getMUT() {
@@ -79,7 +74,7 @@ public Term getPreConTerm() {
         if (c instanceof FunctionalOperationContract t) {
             OriginalVariables orig = t.getOrigVars();
             Term post = t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
-                orig.params, orig.atPres, services);
+                    orig.params, orig.atPres, services);
             return post;
         }
         // no pre <==> false
@@ -170,7 +165,7 @@ private String processUpdate(Term update) {
                 return "";
             }
             return "   \n" + up.lhs().sort() + " " + up.lhs().toString() + " = " + update.sub(0)
-                + ";";
+                    + ";";
         }
         StringBuilder result = new StringBuilder();
         for (Term sub : update.subs()) {

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/RefEx.java

@@ -3,28 +3,17 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.testgen;
 
+import org.jspecify.annotations.Nullable;
+
 /**
- * Reference expression
+ * Reference expression.
+ * <p>
+ * Example: rcObj.field, where rcObjType is the type of rcObj. The prefix "rc" stands for
+ * receiver.
  *
  * @author gladisch
  */
-public class RefEx {
-    public final String rcObjType;
-    public final String rcObj;
-    public final String fieldType;
-    public final String field;
-
-    /**
-     * Example: rcObj.field, where rcObjType is the type of rcObj. The prefix "rc" stands for
-     * receiver.
-     */
-    public RefEx(String rcObjType, String rcObj, String fieldType, String field) {
-        this.rcObjType = rcObjType;
-        this.rcObj = rcObj;
-        this.fieldType = fieldType;
-        this.field = field;
-    }
-
+public record RefEx(@Nullable String rcObjType, String rcObj, String fieldType, String field) {
     @Override
     public String toString() {
         if (rcObjType != null && !rcObjType.isEmpty()) {