Improvements

Author: rcosta358

examples.md

@@ -11,7 +11,7 @@ Start with the full examples repository when you want a runnable setup, then use
 
 To try out the examples, you can:
 
-- Clone locally: `git clone {{ site.liquidjava_examples_url }}.git`
+- Clone locally: `git clone {{ site.liquidjava_examples_url }}`
 - Open in the cloud: [GitHub Codespaces]({{ site.liquidjava_examples_codespaces_url }})
 
 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.

getting-started/index.md

@@ -8,13 +8,10 @@ description: Start with the LiquidJava basics, from overview to installation and
 cards:
   - title: Overview
     url: /getting-started/overview/
-    description: Learn what LiquidJava adds to Java and how the documentation is organized.
+    description: Learn what LiquidJava adds to Java.
   - title: Installation
     url: /getting-started/installation/
     description: Set up the API, verifier, and editor tooling needed to start checking Java code.
-  - title: Quickstart
-    url: /getting-started/quickstart/
-    description: Follow a short end-to-end example that introduces refinements and verification feedback.
 ---
 
 # Getting Started

getting-started/installation.md

@@ -7,20 +7,12 @@ description: Install the LiquidJava annotation API and choose between the VS Cod
 
 # Installation
 
-LiquidJava has two pieces in practice:
-
-- the `liquidjava-api` annotations added to your Java project
-- a verifier workflow, either through VS Code or through the command line
-
 ## Requirements
 
-- Java 20+
-- Maven 3.6+
+- Java 17 or newer
+- Maven 3.6 or newer
 - Visual Studio Code, if you want the extension workflow
-
-## Add the Annotation API
-
-Use the annotation dependency from Maven Central.
+- The `liquidjava-api` dependency in the Java project you want to verify
 
 ### Maven
 
@@ -44,32 +36,34 @@ dependencies {
 }
 ```
 
-## Option 1: VS Code Extension
+You can work use LiquidJava in two ways:
+
+- Through the [VS Code extension]({{ '/tooling/vscode-extension/' | relative_url }})
+- Through the [command-line interface]({{ '/tooling/cli/' | relative_url }})
+
+## VS Code Extension
 
 The easiest setup for most users is:
 
-1. Install the [LiquidJava VS Code extension](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java).
-2. Install [Language Support for Java by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java).
-3. Open a Maven-based Java project that already includes `liquidjava-api`.
+1. Install the [LiquidJava VS Code extension](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java)
+2. Install [Language Support for Java by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java)
+3. Open a Java project with the `liquidjava-api` dependency
+
+The extension then provides real-time diagnostics, syntax highlighting for refinements, and more.
 
-The extension then provides live diagnostics, syntax highlighting for refinements, and richer diagnostic views.
+You can find more about the extension [here]({{ '/tooling/vscode-extension/' | relative_url }}).
 
-## Option 2: Build the Verifier Locally
+## Command Line Interface
 
 If you want the command-line verifier directly:
 
 ```bash
-git clone {{ site.liquidjava_repo_url }}.git
+git clone {{ site.liquidjava_repo_url }}
 cd liquidjava
-./mvnw clean install
+mvn clean install
+./liquidjava /path/to/your/project
 ```
 
-If you prefer system Maven, `mvn clean install` works as well.
-
-## Verify the Installation
-
-- Open [Quickstart]({{ '/getting-started/quickstart/' | relative_url }}) and run the sample verifier command.
-- Or open [Examples]({{ '/examples/' | relative_url }}) and try the example repository in Codespaces or locally.
+This runs the verifier on your project and prints any errors to the console.
 
-{: .note }
-The VS Code extension still expects the `liquidjava-api` dependency in the project being checked.
+You can find more about the command-line interface [here]({{ '/tooling/cli/' | relative_url }}).

getting-started/overview.md

@@ -7,52 +7,33 @@ description: Learn what LiquidJava adds to Java, which problems it solves, and w
 
 # Overview
 
-LiquidJava is an additional type checker for Java. It extends Java with three main specification tools:
+LiquidJava is an additional type checker for Java. It extends Java with three main features:
 
-- **Refinement types** to restrict the values variables, parameters, and return values may take.
+- **Liquid types** to restrict the values variables, parameters, and return values can have using logical predicates.
 - **Typestates** to describe valid object protocols across method calls.
-- **Ghost variables** to track extra state when a protocol depends on counters or flags rather than named states alone.
+- **Ghost variables** to track extra state when typestates aren't enough.
 
-At a high level, LiquidJava helps catch mistakes that ordinary Java typing does not express well, including:
+At a high level, LiquidJava helps catch mistakes that the standard Java type system cannot, including:
 
-- division by zero
-- values falling outside accepted ranges
-- invalid call sequences such as using an object after it is closed
-- incorrect use of external library types that have been refined separately
+- Division by zero
+- Array index out-of-bounds
+- Values falling outside valid ranges
+- Invalid protocol usages such as reading a file after it is closed
 
-## A Small Example
+## Example
 
 ```java
-import liquidjava.specification.Refinement;
+import liquidjava.specification.*;
 
 public class Example {
     public static int divide(int a, @Refinement("b != 0") int b) {
         return a / b;
     }
-
     public static void main(String[] args) {
-        int ok = divide(8, 2);
-        int bad = divide(8, 0); // verification error
+        int result = divide(1, 0); // type error!
     }
 }
 ```
 
-The refinement on `b` states that callers must provide a non-zero argument. Instead of waiting for a runtime exception, LiquidJava rejects the invalid call during verification.
-
-## What You Need
-
-- Java 20 or newer
-- Maven 3.6 or newer
-- The `liquidjava-api` dependency in the Java project you want to verify
-
-You can work with LiquidJava in two main ways:
-
-- through the [VS Code extension]({{ '/tooling/vscode-extension/' | relative_url }}) for an editor-first workflow
-- through the [CLI verifier]({{ '/tooling/cli/' | relative_url }}) for direct command-line verification
-
-## Documentation Map
-
-- Start with [Installation]({{ '/getting-started/installation/' | relative_url }}) to set up the API and tooling.
-- Follow [Quickstart]({{ '/getting-started/quickstart/' | relative_url }}) for a concise first run.
-- Use the [Reference]({{ '/reference/' | relative_url }}) section to learn the annotation model in more detail.
-- Visit [Examples]({{ '/examples/' | relative_url }}) when you want runnable projects.
+The refinement on `b` states that callers must provide a non-zero argument, which is checked at compile time using an [SMT solver](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories).
+The call `divide(1, 0)` violates this contract, so the verifier reports an error without the program even running.

getting-started/quickstart.md

@@ -3,11 +3,8 @@ title: LiquidJava Docs
 layout: default
 nav_exclude: true
 has_toc: false
-description: Start with installation, quickstart, runnable examples, and reference material for LiquidJava.
+description: Start with installation, runnable examples, and reference material for LiquidJava.
 cards:
-  - title: Quickstart
-    url: /getting-started/quickstart/
-    description: Install the annotation API, run the verifier, and see a failing refinement in a few minutes.
   - title: VS Code Extension
     url: /tooling/vscode-extension/
     description: Use real-time diagnostics, syntax highlighting, and state-machine visualizations directly in the editor.
@@ -31,7 +28,7 @@ cards:
 
   <div class="home-actions">
     <a class="home-button primary" href="{{ '/getting-started/installation/' | relative_url }}">Install LiquidJava</a>
-    <a class="home-button secondary" href="{{ '/getting-started/quickstart/' | relative_url }}">Learn More</a>
+    <a class="home-button secondary" href="{{ '/getting-started/overview/' | relative_url }}">Learn More</a>
   </div>
 
   <div class="home-banner">

index.md

@@ -11,7 +11,7 @@ LiquidJava ships with a command-line entry point for verifying Java files or pro
 ## Build the Project
 
 ```bash
-git clone {{ site.liquidjava_repo_url }}.git
+git clone {{ site.liquidjava_repo_url }}
 cd liquidjava
 ./mvnw clean install
 ```
@@ -43,5 +43,3 @@ mvn exec:java -pl liquidjava-verifier \
 - quick local experiments
 - environments where you do not want to rely on VS Code
 - debugging verifier behavior separately from editor integration
-
-For a faster first experience, the [Quickstart]({{ '/getting-started/quickstart/' | relative_url }}) page uses the same command on a tiny example.