Skip to content

Commit 1f73190

Browse files
committed
Minor Changes
1 parent c04cda0 commit 1f73190

File tree

5 files changed

+15
-86
lines changed

5 files changed

+15
-86
lines changed

examples.md

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,4 @@ description: LiquidJava example usages with focused code snippets.
77

88
# Examples
99

10-
Start with the full examples repository when you want a runnable setup, then use the snippets below as a map to the kinds of specifications you will find there.
11-
12-
To try out the examples, you can:
13-
14-
- Clone locally: `git clone {{ site.liquidjava_examples_url }}`
15-
- Open in the cloud: [GitHub Codespaces]({{ site.liquidjava_examples_codespaces_url }})
16-
17-
Once the project is open, use the [VS Code extension]({{ site.liquidjava_vscode_extension_url }}) to run automatically run the verifier and view diagnostics directly in the editor.
18-
19-
TODO: Add examples
10+
TODO

reference/ghosts.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ public interface StackRefinements<E> {
2828
@StateRefinement(from="size() > 0")
2929
public E peek();
3030
}
31-
````
31+
```
3232

3333
```java
3434
Stack<String> s = new Stack<>();

reference/state-refinements.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ If no `to` transition is written, LiquidJava defaults the constructor to the fir
5959

6060
Constructors must always be present for typestate checking to work correctly, because they are the point where the initial state values are assigned. Otherwise, the initial values are not set and the verifier won't be able to track the state of the object across method calls, which can lead to unexpected type errors.
6161

62-
When refining interfaces, there is no real constructor, but LiquidJava still needs an initialization point. In those cases, if the type is named `Interface`, it must declare a method with the signature `public void Interface()` so the initial values are set correctly. This method plays the role of a constructor for the typestate system.
62+
When refining interfaces, which cannot have a constructor, LiquidJava still needs an initialization point. In those cases, the refinement interface must declare a method whose name matches the class we are refining. For example, an interface named `ArrayListRefinements` that is refining `java.util.ArrayList` should declare the method `public void ArrayList()`. This method plays the role of a constructor for the typestate system and ensures the initial values are set correctly.
6363

6464

6565
## Multiple StateSets

tooling/cli.md

Lines changed: 4 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -4,42 +4,8 @@ nav_order: 5
44
description: Run the LiquidJava verifier from the command line for local checks, debugging, and CI workflows.
55
---
66

7-
# Command Line
7+
# Command-Line Interface
88

9-
LiquidJava ships with a command-line entry point for verifying Java files or projects outside the editor flow.
10-
11-
## Build the Project
12-
13-
```bash
14-
git clone {{ site.liquidjava_repo_url }}
15-
cd liquidjava
16-
./mvnw clean install
17-
```
18-
19-
## Run the Wrapper Script
20-
21-
The repository includes a helper script named `liquidjava`:
22-
23-
```bash
24-
./liquidjava /path/to/your/project
25-
```
26-
27-
Internally it runs:
28-
29-
```bash
30-
mvn exec:java -pl liquidjava-verifier \
31-
-Dexec.mainClass="liquidjava.api.CommandLineLauncher" \
32-
-Dexec.args="/path/to/your/project"
33-
```
34-
35-
## Example Outcomes
36-
37-
- A correct file should pass verification.
38-
- A file that violates a refinement should produce an error that points to the failed contract.
39-
40-
## When to Use the CLI
41-
42-
- CI or scripted checks
43-
- quick local experiments
44-
- environments where you do not want to rely on VS Code
45-
- debugging verifier behavior separately from editor integration
9+
TODO:
10+
- Flags and options
11+
- Example usage

tooling/vscode-extension.md

Lines changed: 8 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -6,39 +6,11 @@ description: Install the LiquidJava VS Code extension for live verification, syn
66

77
# VS Code Extension
88

9-
The VS Code extension is the smoothest way to work with LiquidJava day to day.
10-
11-
## What It Adds
12-
13-
- real-time verification diagnostics
14-
- syntax highlighting for refinement annotations
15-
- richer diagnostic details in a webview
16-
- state-machine visualizations for protocol-oriented specifications
17-
18-
## Install
19-
20-
- Install [LiquidJava on the VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) or [Open VSX](https://open-vsx.org/extension/AlcidesFonseca/liquid-java).
21-
- Install [Language Support for Java by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java).
22-
- Open a Java project that includes the `liquidjava-api` dependency.
23-
24-
## Example Dependency
25-
26-
```xml
27-
<dependency>
28-
<groupId>io.github.liquid-java</groupId>
29-
<artifactId>liquidjava-api</artifactId>
30-
<version>{{ site.liquidjava_api_version }}</version>
31-
</dependency>
32-
```
33-
34-
## Best Way to Try It
35-
36-
The [examples repository]({{ site.liquidjava_examples_url }}) is set up for experimentation and can be opened directly in [GitHub Codespaces]({{ site.liquidjava_examples_codespaces_url }}).
37-
38-
## Source
39-
40-
- [Extension source repository](https://github.com/liquid-java/vscode-liquidjava)
41-
- [Main LiquidJava repository]({{ site.liquidjava_repo_url }})
42-
43-
{: .tip }
44-
If you want to understand the annotation language before installing tooling, start with [Refinements]({{ '/reference/refinements/' | relative_url }}).
9+
TODO:
10+
- Real-time verification diagnostics
11+
- Syntax highlighting for refinements
12+
- Autocomplete for refinements
13+
- Webview - diagnostic explorer, context debugger, state machine visualizer
14+
- Status bar indicator
15+
- Commands
16+
- Log output channel

0 commit comments

Comments
 (0)