diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml
index 5b42f4cb..d3aeacf0 100644
--- a/liquidjava-verifier/pom.xml
+++ b/liquidjava-verifier/pom.xml
@@ -38,6 +38,46 @@
20
+
+
+ org.jacoco
+ jacoco-maven-plugin
+ 0.8.14
+
+
+ default-prepare-agent
+
+ prepare-agent
+
+
+
+ default-report
+
+ report
+
+
+
+ default-check
+
+ check
+
+
+
+
+ BUNDLE
+
+
+ COMPLEXITY
+COVEREDRATIO
+0.4
+
+
+
+
+
+
+
+
org.apache.maven.plugins
maven-compiler-plugin
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/CommandLineLauncherIntegrationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/CommandLineLauncherIntegrationTest.java
new file mode 100644
index 00000000..ba435644
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/CommandLineLauncherIntegrationTest.java
@@ -0,0 +1,73 @@
+package liquidjava.verifier.integration;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.io.*;
+import java.nio.file.*;
+import java.util.*;
+
+import org.junit.jupiter.api.*;
+
+public class CommandLineLauncherIntegrationTest {
+
+ private static final String VERIFIER_MAIN = "liquidjava.api.CommandLineLauncher";
+
+ @BeforeAll
+ static void setup() {
+ // se necessário: compilar os exemplos ou garantir que os ficheiros de teste existem
+ }
+
+ @Test
+ void testCorrectExampleShouldPassVerification() throws Exception {
+ // supondo que existe no projecto um ficheiro de exemplo “CorrectSimpleAssignment.java”
+ Path example = Paths.get("liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java");
+ assertTrue(Files.exists(example), "Ficheiro de exemplo correcto não encontrado: " + example);
+
+ ProcessBuilder pb = new ProcessBuilder(
+ "java",
+ "-cp",
+ System.getProperty("java.class.path"),
+ VERIFIER_MAIN,
+ example.toString()
+ );
+ pb.redirectErrorStream(true);
+ Process process = pb.start();
+
+ String output;
+ try (BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()))) {
+ output = reader.lines().reduce("", (a,b) -> a + b + System.lineSeparator());
+ }
+ int exitCode = process.waitFor();
+ // verificar que passou
+ assertEquals(0, exitCode, "Exit code devia ser 0 para caso correcto. Output:\n" + output);
+ assertTrue(output.contains("Correct! Passed Verification") || output.contains("Passed Verification"),
+ "Output inesperado para caso correcto: " + output);
+ }
+
+ @Test
+ void testErrorExampleShouldFailVerification() throws Exception {
+ // supondo que existe o ficheiro “ErrorSimpleAssignment.java”
+ Path example = Paths.get("liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java");
+ assertTrue(Files.exists(example), "Ficheiro de exemplo de erro não encontrado: " + example);
+
+ ProcessBuilder pb = new ProcessBuilder(
+ "java",
+ "-cp",
+ System.getProperty("java.class.path"),
+ VERIFIER_MAIN,
+ example.toString()
+ );
+ pb.redirectErrorStream(true);
+ Process process = pb.start();
+
+ String output;
+ try (BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()))) {
+ output = reader.lines().reduce("", (a,b) -> a + b + System.lineSeparator());
+ }
+ int exitCode = process.waitFor();
+ // verificar que falhou
+ assertNotEquals(0, exitCode, "Exit code devia ser diferente de 0 para caso de erro. Output:\n" + output);
+ assertTrue(output.toLowerCase().contains("error") || output.contains("Refinement violation"),
+ "Output inesperado para caso de erro: " + output);
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestIntegration.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestIntegration.java
new file mode 100644
index 00000000..9bcf7956
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestIntegration.java
@@ -0,0 +1,19 @@
+package liquidjava.integration;
+
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.opt.ConstantFolding;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+
+public class TestIntegration {
+ @Test
+ public void testConstantFoldingIntegration() {
+ BinaryExpression expr = new BinaryExpression(new LiteralInt(3), "*", new LiteralInt(4));
+ ValDerivationNode result = ConstantFolding.fold(new ValDerivationNode(expr, null));
+ assertEquals(new LiteralInt(12), result.getValue());
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestLiteralString.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestLiteralString.java
new file mode 100644
index 00000000..7e82772f
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestLiteralString.java
@@ -0,0 +1,14 @@
+package liquidjava.rj_language;
+
+import static org.junit.Assert.assertNotEquals;
+import org.junit.Test;
+import liquidjava.rj_language.ast.LiteralString;
+
+public class TestLiteralString {
+ @Test
+ public void testLiteralString() {
+ LiteralString s1 = new LiteralString("hello");
+ LiteralString s2 = new LiteralString("world");
+ assertNotEquals(s1.hashCode(), s2.hashCode());
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/TestOptimization.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/TestOptimization.java
new file mode 100644
index 00000000..cdf819a8
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/TestOptimization.java
@@ -0,0 +1,18 @@
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.opt.ConstantFolding;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+
+public class TestOptimization {
+ @Test
+ public void testBinaryFold() {
+ BinaryExpression b = new BinaryExpression(new LiteralInt(1), "+", new LiteralInt(2));
+
+ ValDerivationNode r = ConstantFolding.fold(new ValDerivationNode(b, null));
+ assertEquals(r.getValue(), new LiteralInt(3));
+ }
+}