Merge branch 'main' of https://github.com/CatarinaGamboa/liquidjava

Author: CatarinaGamboa

.git-blame-ignore-revs

@@ -0,0 +1 @@
+012a81397062e33d44d9dbc5974c44483ca4763b

.github/workflows/maven.yml

@@ -10,11 +10,11 @@ name: Java CI with Maven
 
 on:
   push:
-    branches: [ "master" ]
+    branches: [ "main" ]
   pull_request:
-    branches: [ "master" ]
+    branches: [ "main" ]
+
 
-   
 
 jobs:
   build:

.pre-commit-config.yaml

@@ -1,6 +1,15 @@
+# See https://pre-commit.com for more information
+# See https://pre-commit.com/hooks.html for more hooks
 repos:
-- repo: https://github.com/ejba/pre-commit-maven
-  rev: v0.3.3
-  hooks:
-  - id: maven
-    args: [clean compile]
+  - repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v5.0.0
+    hooks:
+      - id: trailing-whitespace
+      - id: end-of-file-fixer
+      - id: check-yaml
+      - id: check-added-large-files
+  - repo: https://github.com/macisamuele/language-formatters-pre-commit-hooks
+    rev: v2.14.0
+    hooks:
+      - id: pretty-format-java
+        args: [--palantir, --autofix]

.vscode/settings.json

@@ -1,3 +1,3 @@
 {
     "java.configuration.updateBuildConfiguration": "automatic"
-}
+}

README.md

@@ -2,65 +2,65 @@
 
 ![LiquidJava Banner](docs/design/figs/banner.gif)
 
+## Welcome to LiquidJava
 
-### Welcome to LiquidJava!
-
-LiquidJava is an additional typechecker for Java that supports liquid types and typestate.
+LiquidJava is an additional type checker for Java that based on liquid types and typestates.
 
 Simple example:
 
-
 ```java
 @Refinement("a > 0")
 int a = 3; // okay
 a = -8; // type error!
 ```
 
-This project has the LiquidJava verifier, the api and some examples for testing.
+This project has the LiquidJava verifier, the API and some examples for testing.
 You can find out more about LiquidJava in the following resources:
 
 * [Website](https://catarinagamboa.github.io/liquidjava.html)
 * [Examples of LiquidJava](https://github.com/CatarinaGamboa/liquidjava-examples)
-* [LiquidJava Specification of Java StdLib](https://github.com/CatarinaGamboa/liquid-java-external-libs)
+* [LiquidJava Specification of the Java Standard Library](https://github.com/CatarinaGamboa/liquid-java-external-libs)
 * [VSCode plugin for LiquidJava](https://github.com/CatarinaGamboa/vscode-liquidjava)
 <!-- * [Formalization of LiquidJava](https://github.com/CatarinaGamboa/liquidjava-formalization) - not opensource yet -->
 
-
 ## 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` in `liquidjava-umbrella` to `compile` and run the `tests`
+4. Use the `pom.xml` in the root directory (which your IDE may have renamed to`liquidjava-umbrella`) to compile and run the tests.
 
 ## Run verification
-#### In a specific project
+
+### In a specific project
+
 Run the file `liquidjava-verifier\api\CommandLineLaucher` with the path to the target project for verification.
 If there are no arguments given, the application verifies the project on the path `liquidjava-example\src\main\java`.
 
-
 ## Testing
-Run `mvn test` to run all the tests in liquidjava.
 
-The starter test file is `TestExamples.java` which uses the test suite under the `liquidjava-examples/testSuite`. 
+Run `mvn test` to run all the tests in LiquidJava.
+
+The starter test file is `TestExamples.java` which uses the test suite under the `liquidjava-examples/testSuite`.
+
+Paths in the test suite are considered test cases if:
 
-Paths in the testSuite are considered test cases if:
 1. File that start with `Correct` or `Error` (e.g, "CorrectRecursion.java")
 2. Package/Folder that contains the word `correct` or `error`.
 
 Therefore, files/folders that do not pass this description are not verified.
 
 ## Project structure
-- **docs**: documents used for the design of the language. The folder includes a readme to a full artifact used in the design process, here are some initial documents used to prepare the design of the refinements language at its evaluation
-- **liquidjava-api**: inlcudes the annotations that can be introduced in the Java programs to add the refinements
-- **liquidjava-examples**: includes a main folder with the current example that the verifier is testing; the test suite that is used in maven test is under the `testSuite` folder
-- **liquidjava-verifier**: has the project for verification of the classes
-    - *api*: classes that test the verifier. Includes the `CommandLineLauncher` that runs the verification on a given class or on the main folder of `liquidjava-examples` if no argument is given. This package includes the JUnit tests to verify if the examples in `liquidjava-example/tests` are correctly verified.
-    - *ast*: represents the abstract syntax tree of the refinement's language.
-    - *errors*: package for reporting the errors.
-    - *processor*: package that handles the type checking.
-    - *rj_language*: handles the processing of the strings with refinements.
-    - *smt*: package that handles the translation to the smt solver and the processing of the results the smt solver produces.
-    - *utils*: includes useful methods for all the previous packages.
-    - *test/java/liquidjava/api/tests* contains the `TestExamples` class used for running the testSuite
-
 
+* **docs**: documents used for the design of the language. The folder includes a readme to a full artifact used in the design process, here are some initial documents used to prepare the design of the refinements language at its evaluation
+* **liquidjava-api**: inlcudes the annotations that can be introduced in the Java programs to add the refinements
+* **liquidjava-examples**: includes a main folder with the current example that the verifier is testing; the test suite that is used in maven test is under the `testSuite` folder
+* **liquidjava-verifier**: has the project for verification of the classes
+  * *api*: classes that test the verifier. Includes the `CommandLineLauncher` that runs the verification on a given class or on the main folder of `liquidjava-examples` if no argument is given. This package includes the JUnit tests to verify if the examples in `liquidjava-example/tests` are correctly verified.
+  * *ast*: represents the abstract syntax tree of the refinement's language.
+  * *errors*: package for reporting the errors.
+  * *processor*: package that handles the type checking.
+  * *rj_language*: handles the processing of the strings with refinements.
+  * *smt*: package that handles the translation to the SMT solver and the processing of the results the SMT solver produces.
+  * *utils*: includes useful methods for all the previous packages.
+  * *test/java/liquidjava/api/tests* contains the `TestExamples` class used for running the test suite.