Cleanup: Use Standard Tech for Test Fixtures

build.gradle

@@ -87,10 +87,7 @@ subprojects {
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.16")
         implementation("org.slf4j:slf4j-api:2.0.16")
-        testImplementation("ch.qos.logback:logback-classic:1.5.15")
 
-        //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0'
-        //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
 
         compileOnly("org.jspecify:jspecify:1.0.0")
         testCompileOnly("org.jspecify:jspecify:1.0.0")
@@ -101,11 +98,18 @@ subprojects {
         checkerFramework "io.github.eisop:checker-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker:$eisop_version"
 
+        testImplementation("org.assertj:assertj-core:3.27.3")
         testImplementation("ch.qos.logback:logback-classic:1.5.15")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.4'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.4'
         testImplementation project(':key.util')
 
+        // test fixtures
+        testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.18.2")
+        testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.18.2")
+
+
+
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.4'
     }
 
@@ -140,7 +144,6 @@ subprojects {
 
     tasks.withType(Test) {
         useJUnitPlatform {
-            includeEngines 'junit-vintage'
             includeEngines 'junit-jupiter'
         }
     }

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.12.1-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core/src/test/java/de/uka/ilkd/key/macros/scripts/TestProofScriptCommand.java

@@ -3,17 +3,14 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros.scripts;
 
-import java.io.BufferedReader;
-import java.io.FileNotFoundException;
+import java.io.File;
 import java.io.IOException;
 import java.net.URISyntaxException;
-import java.net.URL;
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.util.ArrayList;
 import java.util.List;
-import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -22,91 +19,93 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.smt.newsmt2.MasterHandlerTest;
-import de.uka.ilkd.key.util.LineProperties;
 
 import org.key_project.util.collection.ImmutableList;
 
+import com.fasterxml.jackson.databind.ObjectMapper;
+import com.fasterxml.jackson.dataformat.yaml.YAMLFactory;
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.Arguments;
 import org.junit.jupiter.params.provider.MethodSource;
 
+import static org.assertj.core.api.Assertions.assertThat;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
-
 /**
  * see {@link MasterHandlerTest} from where I copied quite a bit.
  */
 public class TestProofScriptCommand {
-    public static List<Arguments> data() throws IOException, URISyntaxException {
-        URL url = TestProofScriptCommand.class.getResource("cases");
-        if (url == null) {
-            throw new FileNotFoundException("Cannot find resource 'cases'.");
-        }
-
-        if (!url.getProtocol().equals("file")) {
-            throw new IOException("Resource should be a file URL not " + url);
-        }
+    public record TestInstance(String key, String script, String exception,
+            String[] goals, Integer selectedGoal) {
+    }
 
-        Path directory = Paths.get(url.toURI());
-        assertTrue(Files.isDirectory(directory));
-        try (var s = Files.list(directory)) {
-            return s.map(f -> Arguments.of(f.getFileName().toString(), f))
-                    .collect(Collectors.toList());
+    public static List<Arguments> data() throws IOException, URISyntaxException {
+        var folder = Paths.get("src/test/resources/de/uka/ilkd/key/macros/scripts");
+        try (var walker = Files.walk(folder)) {
+            List<Path> files =
+                walker.filter(it -> it.getFileName().toString().endsWith(".yml")).toList();
+            var objectMapper = new ObjectMapper(new YAMLFactory());
+            objectMapper.findAndRegisterModules();
+
+            List<Arguments> args = new ArrayList(files.size());
+            for (Path path : files) {
+                try {
+                    TestInstance instance =
+                        objectMapper.readValue(path.toFile(), TestInstance.class);
+                    args.add(Arguments.of(path.toFile(), instance));
+                } catch (Exception e) {
+                    System.out.println(path);
+                    e.printStackTrace();
+                    throw e;
+                }
+            }
+            return args;
         }
     }
 
     @ParameterizedTest
     @MethodSource("data")
-    void testProofScript(String name, Path path) throws Exception {
-
-        BufferedReader reader = Files.newBufferedReader(path);
-        LineProperties props = new LineProperties();
-        props.read(reader);
-
-        List<String> lines = new ArrayList<>(props.getLines("KeY"));
+    void testProofScript(File file, TestInstance data) throws Exception {
+        var name = file.getName().replace(".yml", "");
         Path tmpKey = Files.createTempFile("proofscript_key_" + name, ".key");
-        Files.write(tmpKey, lines);
+        Files.writeString(tmpKey, data.key());
 
         KeYEnvironment<DefaultUserInterfaceControl> env = KeYEnvironment.load(tmpKey.toFile());
 
         Proof proof = env.getLoadedProof();
 
-        String script = props.get("script");
-        ProofScriptEngine pse =
-            new ProofScriptEngine(script,
-                new Location(path.toUri(), Position.newOneBased(1, 1)));
+        ProofScriptEngine pse = new ProofScriptEngine(data.script(),
+            new Location(file.toURI(), Position.newOneBased(1, 1)));
 
+        boolean hasException = data.exception() != null;
         try {
             pse.execute(env.getUi(), proof);
         } catch (Exception ex) {
-            assertTrue(props.containsKey("exception"), "unexpected exception");
-            Assertions.assertEquals(ex.getMessage(), props.get("exception").trim());
+            assertTrue(hasException,
+                "An exception was not expected, but got " + ex.getClass());
+            assertThat(data.exception.trim())
+                    .startsWithIgnoringCase(ex.getMessage().trim().replace("\r\n", "\n"));
             return;
         }
 
-        Assertions.assertFalse(props.containsKey("exception"),
+        Assertions.assertFalse(hasException,
             "exception would have been expected");
 
-        ImmutableList<Goal> goals = proof.openGoals();
-        if (props.containsKey("goals")) {
-            int expected = Integer.parseInt(props.get("goals").trim());
+        if (data.goals() != null) {
+            ImmutableList<Goal> goals = proof.openGoals();
+            int expected = data.goals().length;
             Assertions.assertEquals(expected, goals.size());
-        }
-
 
-        int no = 1;
-        while (props.containsKey("goal " + no)) {
-            String expected = props.get("goal " + no).trim();
-            Assertions.assertEquals(expected, goals.head().toString().trim(), "goal " + no);
-            goals = goals.tail();
-            no++;
-        }
+            for (String expectedGoal : data.goals()) {
+                assertThat(goals.head().toString().trim()).isEqualTo(expectedGoal);
+                goals = goals.tail();
+            }
 
-        if (props.containsKey("selected")) {
-            Goal goal = pse.getStateMap().getFirstOpenAutomaticGoal();
-            String expected = props.get("selected").trim();
-            Assertions.assertEquals(expected, goal.toString().trim());
+            if (data.selectedGoal() != null) {
+                Goal goal = pse.getStateMap().getFirstOpenAutomaticGoal();
+                assertThat(goal.toString().trim()).isEqualTo(data.goals()[data.selectedGoal()]);
+            }
         }
     }