Add regression tests for record methods checked against an external spec (#342)

A record's methods were silently not verified when the project had an
@ExternalRefinementsFor spec: the launcher parsed sources at compliance
level 8, where JDT does not know records. It recovered by turning the
record header into a method `record Repro(int attempts)` and the record's
methods into locals and a block inside it, so the real methods never
existed in the model; the verifier only emitted "Java compilation
encountered issues" and then reported success.

This is already fixed on main by reading the compliance level from the
project's pom (#352), defaulting it to 21 with Spoon 11.5.0 (#368), and
skipping records in the external-spec pass (#370). These directory cases
keep the spec in its own file, as in the issue, and check a record whose
methods violate (and respect) the Throwable typestate.

Fixes #342

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/record_external_spec_correct/Retry.java

@@ -0,0 +1,13 @@
+package testSuite.classes.record_external_spec_correct;
+
+// the methods of a record are checked against an external spec declared in another file (#342)
+public record Retry(int attempts) {
+    void fail(String summary) {
+        Throwable exception = new Throwable(summary);
+        exception.initCause(new RuntimeException("first"));
+    }
+
+    static Throwable wrap(String message, Throwable cause) {
+        return new Throwable(message, cause);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/record_external_spec_correct/ThrowableRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.record_external_spec_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({"withThrowable", "noThrowable"})
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    void Throwable(String message, Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    Throwable initCause(Throwable cause);
+}

liquidjava-example/src/main/java/testSuite/classes/record_external_spec_error/Retry.java

@@ -0,0 +1,15 @@
+package testSuite.classes.record_external_spec_error;
+
+// the methods of a record are checked against an external spec declared in another file (#342)
+public record Retry(int attempts) {
+    void fail(String summary) {
+        Throwable exception = new Throwable(summary, new RuntimeException("first"));
+        exception.initCause(new RuntimeException("second")); // Expect: State Refinement Error
+    }
+
+    static Throwable wrap(String message) {
+        Throwable t = new Throwable(message);
+        t.initCause(new RuntimeException("cause"));
+        return t.initCause(new RuntimeException("again")); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/record_external_spec_error/ThrowableRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.record_external_spec_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({"withThrowable", "noThrowable"})
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    void Throwable(String message, Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    Throwable initCause(Throwable cause);
+}