From 31ec5012b745b3a5adf413149b04ae4f1d1271a7 Mon Sep 17 00:00:00 2001 From: rodrigomilisse Date: Thu, 10 Jul 2025 11:51:52 +0100 Subject: [PATCH 01/10] added basic support for boolean ghost variables --- .../refinement_checker/object_checkers/AuxStateHandler.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index f21329aa..9ff1245e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -83,9 +83,13 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), Predicate.createLit("0", Utils.INT)); c = Predicate.createConjunction(c, p); + } else if (sg.getReturnType().toString().equals("boolean")) { + Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), + Predicate.createLit("false", Utils.BOOLEAN)); + c = Predicate.createConjunction(c, p); } else { // TODO: Implement other stuff - throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in" + throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in" + " AuxStateHandler defaultState"); } } From f1a3f9785d6fe86511ec98a7048e56ae735f5e41 Mon Sep 17 00:00:00 2001 From: rodrigomilisse Date: Fri, 11 Jul 2025 15:56:43 +0100 Subject: [PATCH 02/10] added elementary testing for boolean ghost variables --- .../testBooleanGhost/BooleanGhostClass.java | 39 +++++++++++++++++++ .../testBooleanGhost/BooleanGhostTest.java | 12 ++++++ 2 files changed, 51 insertions(+) create mode 100644 liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java create mode 100644 liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java new file mode 100644 index 00000000..1c08c349 --- /dev/null +++ b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java @@ -0,0 +1,39 @@ +package testBooleanGhost; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("boolean opened") +@Ghost("boolean closed") +public class BooleanGhostClass { + + boolean opened; + boolean closed; + + @StateRefinement(from = "!opened(this) && !closed(this)", to = "opened(this) && !closed(this)") + void open() { + opened = true; + } + + @StateRefinement(from = "opened(this) && !closed(this)") + void execute() { + // System.out.println("opened:" + open + "\nclosed::" + closed); // lança + // exceção + + System.out.println("opened: "); + System.out.println(opened); + System.out.println("\nclosed: "); + System.out.println(closed); + + } + + @StateRefinement(from = "opened(this) && !closed(this)", to = "opened(this) && closed(this)") + void close() { + closed = true; + } + + @StateRefinement(from = "opened(this) && closed(this)") + void terminate() { + System.out.println("Terminating\n"); + } +} diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java new file mode 100644 index 00000000..e8a07d82 --- /dev/null +++ b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java @@ -0,0 +1,12 @@ +package testBooleanGhost; + +public class BooleanGhostTest { + public static void main(String[] args) { + BooleanGhostClass bgc = new BooleanGhostClass(); + + bgc.open(); // ccomment out for error + bgc.execute(); + bgc.close(); // comment out for error + bgc.terminate(); + } +} From bb99e597e233952edcadf81e8d49556a642f9837 Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Fri, 4 Jul 2025 18:13:00 +0100 Subject: [PATCH 03/10] Updated README Setup Instructions --- .gitignore | 1 + README.md | 33 ++++++++++++++++++++++++++++----- 2 files changed, 29 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index dc4a7172..c5c2fd65 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,7 @@ spooned .springBeans .sts4-cache +.idea # Created by https://www.gitignore.io/api/git,java,maven,eclipse,windows diff --git a/README.md b/README.md index deff16f6..8107543d 100644 --- a/README.md +++ b/README.md @@ -24,12 +24,35 @@ You can find out more about LiquidJava in the following resources: * [VSCode plugin for LiquidJava](https://github.com/CatarinaGamboa/vscode-liquidjava) -## Setup the project +# Setup the project -1. Clone the repository; -2. Run `setup.sh`, some dependencies include using `Java 20` or newer and using `Maven`. -3. Open the project in your favorite IDE (we have used Eclipse and VSCode) -4. Use the `pom.xml` in the root directory (which your IDE may have renamed to`liquidjava-umbrella`) to compile and run the tests. +## Installation Steps + +1. Clone the repository: `git clone https://github.com/CatarinaGamboa/liquidjava.git`; +2. Build the project `mvn clean compile`; +3. Run tests to verify installation: `mvn test`; +4. If importing into an IDE, import the project as a Maven project using the root `pom.xml`. + +## Verify Installation + +To verify that everything is working correctly: + +1. **Build the verifier JAR**: + ```bash + mvn package + ``` + +2. **Run verification on examples**: + ```bash + java -jar liquidjava-verifier/target/liquidjava-verifier-5.2-SNAPSHOT.jar liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java + ``` + This should output: `Correct! Passed Verification.` + +3. **Test an error case**: + ```bash + java -jar liquidjava-verifier/target/liquidjava-verifier-5.2-SNAPSHOT.jar liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java + ``` + This should output an error message describing the refinement violation. ## Run verification From 17345d4aaacde94f9f5f4ae9d6d7c13621068154 Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Fri, 4 Jul 2025 18:18:00 +0100 Subject: [PATCH 04/10] Updated README to include Prerequisites --- README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/README.md b/README.md index 8107543d..d4a7a9b0 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,12 @@ You can find out more about LiquidJava in the following resources: # Setup the project +## Prerequisites +Before setting up LiquidJava, ensure you have the following installed: + +- Java 20 or newer - The project is configured to use Java 20; +- Maven 3.6+ - For building and dependency management. + ## Installation Steps 1. Clone the repository: `git clone https://github.com/CatarinaGamboa/liquidjava.git`; From 3396a6da436ccf56676029f369abb551e36ed833 Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Sun, 6 Jul 2025 20:16:45 +0100 Subject: [PATCH 05/10] Updated README installation instructions --- README.md | 27 ++++++++++++++------------- liquidjava-verifier/pom.xml | 3 +++ 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index d4a7a9b0..959dac70 100644 --- a/README.md +++ b/README.md @@ -35,29 +35,30 @@ Before setting up LiquidJava, ensure you have the following installed: ## Installation Steps 1. Clone the repository: `git clone https://github.com/CatarinaGamboa/liquidjava.git`; -2. Build the project `mvn clean compile`; +2. Build the project `mvn clean install`; 3. Run tests to verify installation: `mvn test`; 4. If importing into an IDE, import the project as a Maven project using the root `pom.xml`. ## Verify Installation -To verify that everything is working correctly: +To generate an executable to check your refinements using LiquidJava, do as follows:To verify that you can execute LiquidJava: +*Warning: Any change to LiquidJava requires rebuilding the jar.* -1. **Build the verifier JAR**: - ```bash - mvn package - ``` +1. **Build the jar**: +```bash +mvn package -Djar.finalName=liquidjava +``` 2. **Run verification on examples**: - ```bash - java -jar liquidjava-verifier/target/liquidjava-verifier-5.2-SNAPSHOT.jar liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java - ``` - This should output: `Correct! Passed Verification.` +```bash +java -jar liquidjava-verifier/target/liquidjava.jar liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java +``` + This should output: `Correct! Passed Verification`. 3. **Test an error case**: - ```bash - java -jar liquidjava-verifier/target/liquidjava-verifier-5.2-SNAPSHOT.jar liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java - ``` +```bash +java -jar liquidjava-verifier/target/liquidjava.jar liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java +``` This should output an error message describing the refinement violation. ## Run verification diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index bce34bba..21464fa3 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -17,6 +17,7 @@ jar + ${jar.finalName} net.revelc.code.formatter @@ -110,6 +111,8 @@ 3.8.0 3.1.2 + + ${project.artifactId}-${project.version} From 8ae3216caa3f13a628ec0b957ddb12d6363cfc80 Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Sun, 6 Jul 2025 20:17:53 +0100 Subject: [PATCH 06/10] Fixed typo --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 959dac70..9be65e60 100644 --- a/README.md +++ b/README.md @@ -41,13 +41,14 @@ Before setting up LiquidJava, ensure you have the following installed: ## Verify Installation -To generate an executable to check your refinements using LiquidJava, do as follows:To verify that you can execute LiquidJava: -*Warning: Any change to LiquidJava requires rebuilding the jar.* +To generate an executable to check your refinements using LiquidJava*: 1. **Build the jar**: ```bash mvn package -Djar.finalName=liquidjava ``` +*Warning: Any change to LiquidJava requires rebuilding the jar.* + 2. **Run verification on examples**: ```bash From 2c192080dce13e68ebee05b4429347f8d5fd5f6d Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Sun, 6 Jul 2025 20:32:51 +0100 Subject: [PATCH 07/10] Updated to use mvn --- README.md | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index 9be65e60..d2b66c20 100644 --- a/README.md +++ b/README.md @@ -41,24 +41,17 @@ Before setting up LiquidJava, ensure you have the following installed: ## Verify Installation -To generate an executable to check your refinements using LiquidJava*: - -1. **Build the jar**: -```bash -mvn package -Djar.finalName=liquidjava -``` -*Warning: Any change to LiquidJava requires rebuilding the jar.* - +To check your refinements using LiquidJava: 2. **Run verification on examples**: ```bash -java -jar liquidjava-verifier/target/liquidjava.jar liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java +mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java" ``` This should output: `Correct! Passed Verification`. 3. **Test an error case**: ```bash -java -jar liquidjava-verifier/target/liquidjava.jar liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java +mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java" ``` This should output an error message describing the refinement violation. From 57bbf020bc41796778aa1e9af984c374653956ed Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Sun, 6 Jul 2025 22:03:59 +0100 Subject: [PATCH 08/10] Updated README --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index d2b66c20..922ce221 100644 --- a/README.md +++ b/README.md @@ -43,13 +43,13 @@ Before setting up LiquidJava, ensure you have the following installed: To check your refinements using LiquidJava: -2. **Run verification on examples**: +**Run verification on examples**: ```bash mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java" ``` This should output: `Correct! Passed Verification`. -3. **Test an error case**: +**Test an error case**: ```bash mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java" ``` From 90007dfaed0afb0dcd27460d8ba83e9de0b4bd14 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 9 Oct 2025 11:17:29 +0100 Subject: [PATCH 09/10] Improve Ghost Default Values in AuxStateHandler --- .../object_checkers/AuxStateHandler.java | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 9ff1245e..931de2c1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -79,19 +79,15 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { Predicate c = new Predicate(); List sets = getDifferentSets(tc, klass); // ?? for (GhostFunction sg : sets) { - if (sg.getReturnType().toString().equals("int")) { - Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), - Predicate.createLit("0", Utils.INT)); - c = Predicate.createConjunction(c, p); - } else if (sg.getReturnType().toString().equals("boolean")) { - Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), - Predicate.createLit("false", Utils.BOOLEAN)); - c = Predicate.createConjunction(c, p); - } else { - // TODO: Implement other stuff - throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in" - + " AuxStateHandler defaultState"); - } + String retType = sg.getReturnType().toString(); + Predicate typePredicate = switch (retType) { + case "int" -> Predicate.createLit("0", Utils.INT); + case "boolean" -> Predicate.createLit("false", Utils.BOOLEAN); + case "double" -> Predicate.createLit("0.0", Utils.DOUBLE); + default -> throw new RuntimeException("Ghost not implemented for type " + retType); + }; + Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), typePredicate); + c = Predicate.createConjunction(c, p); } ObjectState os = new ObjectState(); os.setTo(c); From 5aae07e0b9475bf81e48491255b3611dab501611 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 9 Oct 2025 11:17:43 +0100 Subject: [PATCH 10/10] Update Tests --- .../testBooleanGhost/BooleanGhostClass.java | 39 ------------------- .../testBooleanGhost/BooleanGhostTest.java | 12 ------ .../SimpleStateMachine.java | 17 ++++++++ .../boolean_ghost_correct/SimpleTest.java | 10 +++++ .../SimpleStateMachine.java | 17 ++++++++ .../boolean_ghost_error/SimpleTest.java | 10 +++++ .../classes/scoreboard_error/Scoreboard.java | 17 ++++++++ .../classes/scoreboard_error/SimpleTest.java | 11 ++++++ .../vending_machine_correct/SimpleTest.java | 11 ++++++ .../VendingMachine.java | 14 +++++++ liquidjava-verifier/.gitignore | 1 + 11 files changed, 108 insertions(+), 51 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java delete mode 100644 liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleStateMachine.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleStateMachine.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/Scoreboard.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/VendingMachine.java diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java deleted file mode 100644 index 1c08c349..00000000 --- a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java +++ /dev/null @@ -1,39 +0,0 @@ -package testBooleanGhost; - -import liquidjava.specification.Ghost; -import liquidjava.specification.StateRefinement; - -@Ghost("boolean opened") -@Ghost("boolean closed") -public class BooleanGhostClass { - - boolean opened; - boolean closed; - - @StateRefinement(from = "!opened(this) && !closed(this)", to = "opened(this) && !closed(this)") - void open() { - opened = true; - } - - @StateRefinement(from = "opened(this) && !closed(this)") - void execute() { - // System.out.println("opened:" + open + "\nclosed::" + closed); // lança - // exceção - - System.out.println("opened: "); - System.out.println(opened); - System.out.println("\nclosed: "); - System.out.println(closed); - - } - - @StateRefinement(from = "opened(this) && !closed(this)", to = "opened(this) && closed(this)") - void close() { - closed = true; - } - - @StateRefinement(from = "opened(this) && closed(this)") - void terminate() { - System.out.println("Terminating\n"); - } -} diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java deleted file mode 100644 index e8a07d82..00000000 --- a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java +++ /dev/null @@ -1,12 +0,0 @@ -package testBooleanGhost; - -public class BooleanGhostTest { - public static void main(String[] args) { - BooleanGhostClass bgc = new BooleanGhostClass(); - - bgc.open(); // ccomment out for error - bgc.execute(); - bgc.close(); // comment out for error - bgc.terminate(); - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleStateMachine.java b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleStateMachine.java new file mode 100644 index 00000000..c0ad2f90 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleStateMachine.java @@ -0,0 +1,17 @@ +package testSuite.classes.boolean_ghost_correct; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("boolean open") +public class SimpleStateMachine { + + @StateRefinement(from = "!open(this)", to = "open(this)") + void open() {} + + @StateRefinement(from = "open(this)") + void execute() {} + + @StateRefinement(from = "open(this)", to = "!open(this)") + void close() {} +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleTest.java new file mode 100644 index 00000000..48e60423 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleTest.java @@ -0,0 +1,10 @@ +package testSuite.classes.boolean_ghost_correct; + +public class SimpleTest { + public static void main(String[] args) { + SimpleStateMachine ssm = new SimpleStateMachine(); + ssm.open(); + ssm.execute(); + ssm.close(); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleStateMachine.java b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleStateMachine.java new file mode 100644 index 00000000..dd0210b5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleStateMachine.java @@ -0,0 +1,17 @@ +package testSuite.classes.boolean_ghost_error; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("boolean open") +public class SimpleStateMachine { + + @StateRefinement(from = "!open(this)", to = "open(this)") + void open() {} + + @StateRefinement(from = "open(this)") + void execute() {} + + @StateRefinement(from = "open(this)", to = "!open(this)") + void close() {} +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java new file mode 100644 index 00000000..7408096e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java @@ -0,0 +1,10 @@ +package testSuite.classes.boolean_ghost_error; + +public class SimpleTest { + public static void main(String[] args) { + SimpleStateMachine ssm = new SimpleStateMachine(); + ssm.open(); + ssm.close(); + ssm.execute(); // error, not open + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/Scoreboard.java b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/Scoreboard.java new file mode 100644 index 00000000..bb7f47f3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/Scoreboard.java @@ -0,0 +1,17 @@ +package testSuite.classes.scoreboard_error; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("double value") +public class Scoreboard { + + @StateRefinement(from = "value(this) < 1.0", to = "value(this) == value(old(this)) + 0.1") + public void inc() {} + + @StateRefinement(from = "value(this) > 0.0", to = "value(this) == value(old(this)) - 0.1") + public void dec() {} + + @StateRefinement(from = "value(this) > 0.0") + public void finish() {} +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java new file mode 100644 index 00000000..0676175b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java @@ -0,0 +1,11 @@ +package testSuite.classes.scoreboard_error; + +public class SimpleTest { + public static void main(String[] args) { + Scoreboard sb = new Scoreboard(); + sb.inc(); + sb.dec(); + sb.dec(); // error, underflow + sb.finish(); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/SimpleTest.java new file mode 100644 index 00000000..a9101fbc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/SimpleTest.java @@ -0,0 +1,11 @@ +package testSuite.classes.vending_machine_correct; + +public class SimpleTest { + public static void main(String[] args) { + VendingMachine vm = new VendingMachine(); // 30 cents to buy + vm.insertTenCents(); + vm.insertTenCents(); + vm.insertTenCents(); + vm.buy(); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/VendingMachine.java b/liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/VendingMachine.java new file mode 100644 index 00000000..6d40c832 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/VendingMachine.java @@ -0,0 +1,14 @@ +package testSuite.classes.vending_machine_correct; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("double value") +public class VendingMachine { + + @StateRefinement(from = "value(this) >= 0.0", to = "value(this) == value(old(this)) + 0.1") + void insertTenCents() {} + + @StateRefinement(from = "value(this) >= 0.3") + void buy() {} +} \ No newline at end of file diff --git a/liquidjava-verifier/.gitignore b/liquidjava-verifier/.gitignore index 898341b0..d63d510d 100644 --- a/liquidjava-verifier/.gitignore +++ b/liquidjava-verifier/.gitignore @@ -1 +1,2 @@ spooned +.antlr \ No newline at end of file