Skip to content

Commit a9349b7

Browse files
rcosta358rcosta358
authored
Update README's (#59)
1 parent 1262ec3 commit a9349b7

5 files changed

Lines changed: 200 additions & 107 deletions

File tree

‎DEVELOPMENT.md‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
# LiquidJava VS Code Extension Development Guide
2+
3+
### Prerequisites
4+
5+
Before starting development, ensure you have:
6+
7+
- Java 20 or higher installed and configured in your `PATH`
8+
- Maven 3.6 or higher for building the language server
9+
- Node.js and npm for building and packaging the client
10+
- Visual Studio Code and the [Language Support for Java(TM) by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java) extension installed and enabled
11+
12+
### Cloning and Setup
13+
14+
To get started, clone the repository and install the client dependencies:
15+
16+
```bash
17+
git clone https://github.com/liquid-java/vscode-liquidjava.git
18+
cd vscode-liquidjava
19+
cd client
20+
npm install
21+
```
22+
23+
### Packaging and Installation
24+
25+
To build the language server, package the extension, and install it in your local VS Code instance, you can run the provided script from the repository root:
26+
27+
```bash
28+
./install.sh <version>
29+
```
30+
31+
Replace `<version>` with the version number in [client/package.json](./client/package.json).
32+
33+
### Releasing
34+
35+
To create and push a git tag that will trigger the GitHub Actions workflow that automatically publishes the extension in both the [VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) and the [Open VSX Registry](https://open-vsx.org/extension/AlcidesFonseca/liquid-java):
36+
1. Increment the version in [client/package.json](./client/package.json)
37+
2. Run the release script from the repository root:
38+
39+
```bash
40+
./release.sh <new-version>
41+
```
42+
43+
### Development Mode
44+
45+
To run the extension in development mode, follow these steps:
46+
1. Go to **Run** > **Run Extension** (or press **F5**)
47+
2. A new VS Code instance will open with the extension installed, which will automatically run the language server in the background and connect to it
48+
3. Open a Java project using LiquidJava
49+
50+
To run the language server manually, follow these steps:
51+
52+
1. Run the server in port `50000` (default)
53+
2. In the client, set the `DEBUG` constant in [client/src/extension.ts](./client/src/extension.ts) to `true`
54+
3. Run the client which will connect to the server in port `50000`
55+
56+
### Project Structure
57+
- `/server` - Implements the language server in Java using [LSP4J](https://github.com/eclipse/lsp4j)
58+
- `/client` - Implements the VS Code extension in TypeScript that connects to the language server via LSP

‎README.md‎

Lines changed: 112 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,20 @@
11
# LiquidJava VS Code Extension
22

3-
The **LiquidJava VS Code extension** adds support for **refinement types**, extending the Java standard type system directly inside VS Code, using the [LiquidJava](https://github.com/liquid-java/liquidjava) verifier. It provides error diagnostics and syntax highlighting for refinements.
3+
![](https://raw.githubusercontent.com/liquid-java/liquidjava/refs/heads/main/docs/design/figs/banner.gif)
44

5-
## Getting Started
5+
### Extend your Java code with Liquid Types and catch bugs earlier!
66

7-
### GitHub Codespaces
7+
[LiquidJava](https://github.com/liquid-java/liquidjava) is an additional type checker for Java, based on **liquid types** and **typestates**, which provides stronger safety guarantees to Java programs at compile-time. With this extension, you can use LiquidJava directly in VS Code, with real-time diagnostic reporting, syntax highlighting for refinements, and an interactive webview for displaying details about diagnostics and state machine diagrams.
88

9-
To try out the extension on an example project without setting up your local environment:
10-
1. Log in to GitHub
11-
2. Click the button below
12-
3. Select the `4-core` option
13-
4. Press `Create codespace`
14-
15-
The codespace will open in your browser and automatically install the LiquidJava extension shortly.
16-
17-
[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/liquid-java/liquidjava-examples)
9+
```java
10+
@Refinement("a > 0")
11+
int a = 3; // okay
12+
a = -8; // type error!
13+
```
1814

19-
### Local Setup
15+
### Installation
2016

21-
To set up the extension locally, install the LiquidJava extension in the [VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) or the [Open VSX Marketplace](https://open-vsx.org/extension/AlcidesFonseca/liquid-java) and add the `liquidjava-api` dependency to your Java project.
17+
To try out the extension, install it from the [VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) or the [Open VSX Marketplace](https://open-vsx.org/extension/AlcidesFonseca/liquid-java). Additionally, you'll need the [Language Support for Java(TM) by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java) VS Code extension, and add the `liquidjava-api` dependency to your Java project:
2218

2319
#### Maven
2420
```xml
@@ -40,61 +36,105 @@ dependencies {
4036
}
4137
```
4238

43-
## Development
44-
45-
### Developer Mode
46-
47-
To run the extension in developer mode, which automatically spawns the server in a separate process:
48-
49-
1. Open the `client` folder in VS Code
50-
2. Run `npm install`
51-
3. Make sure you have the Red Hat extension for [Language Support for Java™](https://github.com/redhat-developer/vscode-java) installed and enabled
52-
4. Go to `Run` > `Run Extension` (or press `F5`)
53-
5. A new VS Code instance will start with the LiquidJava extension enabled
54-
6. Open a Java project containing the `liquid-java-api.jar` in the `lib` folder
55-
56-
### Debugging Mode
57-
58-
To run the extension in debugging mode by manually starting the server and connecting the client to it:
59-
60-
* Run the server:
61-
- Open the `server` folder in your IDE
62-
- Run `App.java`, which will start the server on port `50000`
63-
- View the server logs in the console
64-
65-
* Run the client:
66-
- Open the `client` folder in VS Code
67-
- Set the `DEBUG` variable to `true` in [`client/src/extension.ts`](./client/src/extension.ts)
68-
- Go to `Run` > `Run Extension` (or press `F5`)
69-
- A new VS Code instance will open with the LiquidJava extension enabled, which will connect to the server on port `50000`
70-
- Open a Java project containing the `liquid-java-api.jar` in the `lib` folder
71-
- View the client logs in the `LiquidJava` output channel or by clicking the status indicator
72-
73-
### Create Server JAR
74-
75-
To build the language server, export it as a runnable JAR file named `language-server-liquidjava.jar` and place it in `/client/server`.
76-
77-
- In **Eclipse**:
78-
- Open the `server` folder
79-
- Select `File > Export > Runnable JAR file`
80-
- In the launch configuration, choose `main - vscode-liquid-java-server`
81-
- In the output path, choose the `/client/server` folder of this extension
82-
- In **VS Code**:
83-
- Open the `server` folder
84-
- Use the Export Jar feature (`Ctrl+Shift+P` > `Java: Export Jar`)
85-
- Select `App` as the main class
86-
- Select `OK`
87-
- Copy the generated JAR from the root directory to the `/client/server` folder
88-
- In **IntelliJ**:
89-
- Open the `server` folder
90-
- Go to `File` > `Project Structure` > `Artifacts`
91-
- Select `Add a new Jar` > `From modules with dependencies`
92-
- Select `App` as the main class
93-
- Build the artifact via `Build` > `Build Artifacts` > `Build`
94-
- Copy the generated JAR from the `out/artifacts` folder to the `/client/server` folder
95-
96-
### Project Structure
97-
- `/server` - Implements the [Language Server Protocol (LSP)](https://microsoft.github.io/language-server-protocol/) in Java using the [LSP4J](https://github.com/eclipse/lsp4j) library
98-
- `/client` - Implements the VS Code extension in TypeScript that connects to the language server using LSP
99-
- It depends on [Language Support for Java™](https://github.com/redhat-developer/vscode-java) for regular Java errors
100-
- `/lib` - Contains the `liquidjava-api.jar` required for the extension to be activated in a Java project
39+
A repository with LiquidJava examples is available at [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples). You can try them out without setting up your local environment using [GitHub Codespaces](https://codespaces.new/liquid-java/liquidjava-examples).
40+
41+
### What are Liquid Types?
42+
43+
Liquid types extend a language with **logical predicates** over the basic types. They allow developers to restrict the values that a variable, parameter or return value can have. These kinds of constraints help to catch more bugs before the program is executed. For example, they allow us to prevent bugs like array index out-of-bounds or division by zero at compile-time.
44+
45+
### LiquidJava
46+
47+
#### Refinements
48+
49+
To refine a variable, field, parameter or return value, use the `@Refinement` annotation with a predicate as an argument. The predicate must be a boolean expression that uses the name of the variable being refined (or `_`) to refer to its value. You can also provide a custom message to be included in the error message when the refinement is violated. Some examples include:
50+
51+
```java
52+
@Refinement("x > 0") // x must be greater than 0
53+
int x;
54+
55+
@Refinement("0 <= _ && _ <= 100") // y must be between 0 and 100
56+
int y;
57+
58+
@Refinement(value="z % 2 == 0 ? z >= 0 : z < 0", msg="z must be positive if even, negative if odd")
59+
int z;
60+
61+
@Refinement("_ >= 0")
62+
int absDiv(int a, @Refinement(value="b != 0", msg="cannot divide by zero") int b) {
63+
int res = a / b;
64+
return res >= 0 ? res : -res;
65+
}
66+
```
67+
68+
#### Refinement Aliases
69+
70+
To simplify the usage of refinements, you can create **predicate aliases** using the `@RefinementAlias` annotation, and apply them inside other refinements:
71+
72+
```java
73+
@RefinementAlias("Percentage(int v) { 0 <= v && v <= 100 }")
74+
public class MyClass {
75+
76+
// x must be between 0 and 100
77+
@Refinement("Percentage(x)")
78+
int x = 25;
79+
}
80+
```
81+
82+
#### Object State Modeling via Typestates
83+
84+
Beyond basic refinements, LiquidJava also supports **object state modeling** via typestates, which allows developers to specify when a method can or cannot be called based on the state of the object. You can also provide a custom error message for when the method precondition is violated. For example:
85+
86+
```java
87+
@StateSet({"open", "closed"})
88+
public class MyFile {
89+
90+
@StateRefinement(to="open(this)")
91+
public MyFile() {}
92+
93+
@StateRefinement(from="open(this)", msg="file must be open to read")
94+
public void read() {}
95+
96+
@StateRefinement(from="open(this)", to="closed(this)", msg="file must be open to close")
97+
public void close() {}
98+
}
99+
100+
MyFile f = new MyFile();
101+
f.read();
102+
f.close();
103+
f.read(); // type error: file must be open to read
104+
```
105+
106+
#### Ghost Variables and External Refinements
107+
108+
Finally, LiquidJava also provides **ghost variables**, which are used to track additional information about the program state when typestates aren't enough, with the `@Ghost` annotation. Additionally, you can also refine external libraries using the `@ExternalRefinementsFor` annotation. Here is an example of the `java.util.Stack` class refined with LiquidJava, using a `size` ghost variable to track the number of elements in the stack:
109+
110+
```java
111+
@ExternalRefinementsFor("java.util.Stack")
112+
@Ghost("int size")
113+
public interface StackRefinements<E> {
114+
115+
public void Stack();
116+
117+
@StateRefinement(to="size(this) == size(old(this)) + 1") // increments size by 1
118+
public boolean push(E elem);
119+
120+
@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1", msg="cannot pop from an empty stack") // decrements size by 1
121+
public E pop();
122+
123+
@StateRefinement(from="size(this) > 0", msg="cannot peek from an empty stack")
124+
public E peek();
125+
}
126+
127+
Stack<String> s = new Stack<>();
128+
s.push("hello");
129+
s.pop();
130+
s.pop(); // type error: cannot pop from an empty stack
131+
132+
```
133+
134+
You can find more examples of how to use LiquidJava on the [LiquidJava Website](https://liquid-java.github.io). To learn how to use LiquidJava, you can also follow the [LiquidJava tutorial](https://github.com/liquid-java/liquidjava-tutorial).
135+
136+
For more information, check the following repositories:
137+
- [liquidjava](https://github.com/liquid-java/liquidjava): Includes the API, verifier and some examples
138+
- [vscode-liquidjava](https://github.com/liquid-java/vscode-liquidjava): Source code of this VS Code extension
139+
- [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples): Examples of how to use LiquidJava
140+
- [liquid-java-external-libs](https://github.com/liquid-java/liquid-java-external-libs): Examples of how to use LiquidJava to refine external libraries

‎client/README.md‎

Lines changed: 28 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
# LiquidJava - Extending Java with Liquid Types
1+
# LiquidJava VS Code Extension
22

33
![](https://raw.githubusercontent.com/liquid-java/liquidjava/refs/heads/main/docs/design/figs/banner.gif)
44

55
### Extend your Java code with Liquid Types and catch bugs earlier!
66

7-
LiquidJava is an additional type checker for Java, based on **liquid types** and **typestates**, which provides stronger safety guarantees to Java programs at compile-time. With this extension, you can use LiquidJava directly in VS Code, with real-time error diagnostics, syntax highlighting for refinements and more!
7+
[LiquidJava](https://github.com/liquid-java/liquidjava) is an additional type checker for Java, based on **liquid types** and **typestates**, which provides stronger safety guarantees to Java programs at compile-time. With this extension, you can use LiquidJava directly in VS Code, with real-time diagnostic reporting, syntax highlighting for refinements, and an interactive webview for displaying details about diagnostics and state machine diagrams.
88

99
```java
1010
@Refinement("a > 0")
@@ -14,8 +14,7 @@ a = -8; // type error!
1414

1515
### Installation
1616

17-
This extension depends on the [Language Support for Java(TM) by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java) VS Code extension.
18-
Additionally, to use LiquidJava in your project, you'll need the following dependency, which includes the LiquidJava annotations:
17+
To try out the extension, install it from the [VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) or the [Open VSX Marketplace](https://open-vsx.org/extension/AlcidesFonseca/liquid-java). Additionally, you'll need the [Language Support for Java(TM) by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java) VS Code extension, and add the `liquidjava-api` dependency to your Java project:
1918

2019
#### Maven
2120
```xml
@@ -37,35 +36,30 @@ dependencies {
3736
}
3837
```
3938

39+
A repository with LiquidJava examples is available at [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples). You can try them out without setting up your local environment using [GitHub Codespaces](https://codespaces.new/liquid-java/liquidjava-examples).
40+
4041
### What are Liquid Types?
4142

42-
Liquid types, or refinement types, extend a language with **logical predicates** over the basic types. They allow developers to restrict the values that a variable, parameter or return value can have. These kinds of constraints help to catch more bugs before the program is executed — for example array index out-of-bounds or division by zero.
43+
Liquid types extend a language with **logical predicates** over the basic types. They allow developers to restrict the values that a variable, parameter or return value can have. These kinds of constraints help to catch more bugs before the program is executed. For example, they allow us to prevent bugs like array index out-of-bounds or division by zero at compile-time.
4344

44-
### Usage
45+
### LiquidJava
4546

4647
#### Refinements
4748

48-
To refine a variable, parameter or return value, use the `@Refinement` annotation with a predicate as an argument. The predicate must be a boolean expression that uses the name of the variable being refined (or `_`) to refer to its value. Some examples include:
49+
To refine a variable, field, parameter or return value, use the `@Refinement` annotation with a predicate as an argument. The predicate must be a boolean expression that uses the name of the variable being refined (or `_`) to refer to its value. You can also provide a custom message to be included in the error message when the refinement is violated. Some examples include:
4950

5051
```java
51-
// x must be greater than 0
52-
@Refinement("x > 0")
52+
@Refinement("x > 0") // x must be greater than 0
5353
int x;
5454

55-
// y must be between 0 and 100
56-
@Refinement("0 <= _ && _ <= 100")
55+
@Refinement("0 <= _ && _ <= 100") // y must be between 0 and 100
5756
int y;
5857

59-
// z must be positive if it is even and negative if it is odd
60-
@Refinement("z % 2 == 0 ? z >= 0 : z < 0")
58+
@Refinement(value="z % 2 == 0 ? z >= 0 : z < 0", msg="z must be positive if even, negative if odd")
6159
int z;
62-
```
6360

64-
Refinements can also be applied to method parameters and return values:
65-
66-
```java
6761
@Refinement("_ >= 0")
68-
int absDiv(int a, @Refinement("b != 0") int b) {
62+
int absDiv(int a, @Refinement(value="b != 0", msg="cannot divide by zero") int b) {
6963
int res = a / b;
7064
return res >= 0 ? res : -res;
7165
}
@@ -85,9 +79,9 @@ public class MyClass {
8579
}
8680
```
8781

88-
#### Object State Modeling with Typestates
82+
#### Object State Modeling via Typestates
8983

90-
Beyond basic refinements, LiquidJava also supports **object state modeling** through typestates, which allows developers to specify when a method can or cannot be called based on the state of the object. For example:
84+
Beyond basic refinements, LiquidJava also supports **object state modeling** via typestates, which allows developers to specify when a method can or cannot be called based on the state of the object. You can also provide a custom error message for when the method precondition is violated. For example:
9185

9286
```java
9387
@StateSet({"open", "closed"})
@@ -96,22 +90,22 @@ public class MyFile {
9690
@StateRefinement(to="open(this)")
9791
public MyFile() {}
9892

99-
@StateRefinement(from="open(this)")
93+
@StateRefinement(from="open(this)", msg="file must be open to read")
10094
public void read() {}
10195

102-
@StateRefinement(from="open(this)", to="closed(this)")
96+
@StateRefinement(from="open(this)", to="closed(this)", msg="file must be open to close")
10397
public void close() {}
10498
}
10599

106-
MyFile f = new MyFile(); // state(f) == "open"
107-
f.read(); // state(f) == "open" (unchanged)
108-
f.close(); // state(f) == "closed"
109-
f.read(); // type error!
100+
MyFile f = new MyFile();
101+
f.read();
102+
f.close();
103+
f.read(); // type error: file must be open to read
110104
```
111105

112106
#### Ghost Variables and External Refinements
113107

114-
Finally, LiquidJava also provides **ghost variables**, which are used to track additional information about the program state when states aren't enough, with the `@Ghost` annotation. Additionally, you can also refine external libraries using the `@ExternalRefinementsFor` annotation. Here is an example of the `java.util.Stack` class refined with LiquidJava, using a `size` ghost variable to track the number of elements in the stack:
108+
Finally, LiquidJava also provides **ghost variables**, which are used to track additional information about the program state when typestates aren't enough, with the `@Ghost` annotation. Additionally, you can also refine external libraries using the `@ExternalRefinementsFor` annotation. Here is an example of the `java.util.Stack` class refined with LiquidJava, using a `size` ghost variable to track the number of elements in the stack:
115109

116110
```java
117111
@ExternalRefinementsFor("java.util.Stack")
@@ -120,20 +114,20 @@ public interface StackRefinements<E> {
120114

121115
public void Stack();
122116

123-
@StateRefinement(to="size(this) == (size(old(this)) + 1)")
117+
@StateRefinement(to="size(this) == size(old(this)) + 1") // increments size by 1
124118
public boolean push(E elem);
125119

126-
@StateRefinement(from="size(this) > 0", to="size(this) == (size(old(this)) - 1)")
120+
@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1", msg="cannot pop from an empty stack") // decrements size by 1
127121
public E pop();
128122

129-
@StateRefinement(from="size(this) > 0")
123+
@StateRefinement(from="size(this) > 0", msg="cannot peek from an empty stack")
130124
public E peek();
131125
}
132126

133-
Stack<Integer> s = new Stack<>(); // size(s) == 0 (default value)
134-
s.push(10); // size(s) == 1
135-
s.pop(); // size(s) == 0
136-
s.pop(); // type error!
127+
Stack<String> s = new Stack<>();
128+
s.push("hello");
129+
s.pop();
130+
s.pop(); // type error: cannot pop from an empty stack
137131

138132
```
139133

0 commit comments

Comments
 (0)