Update Reference Section

Author: rcosta358

reference/external-refinements.md

@@ -11,10 +11,10 @@ External refinements let you attach a LiquidJava model to an existing class that
 Use `@ExternalRefinementsFor` to describe the behavior of a library type in a separate interface. This lets you keep using the original library API in ordinary Java code while LiquidJava checks the extra specification in the background.
 
 ```java
-import liquidjava.specification.ExternalRefinementsFor;
-import liquidjava.specification.StateRefinement;
+import liquidjava.specification.*;
 
 @ExternalRefinementsFor("java.net.Socket")
+@StateSet({"unconnected, bound, connected, closed"})
 public interface SocketRefinements {
     @StateRefinement(to = "unconnected(this)")
     public void Socket();

reference/ghost-variables.md

@@ -21,7 +21,7 @@ public interface StackRefinements<E> {
     public void Stack();
 
     @StateRefinement(to = "size(this) == size(old(this)) + 1")
-    public boolean push(E elem);
+    public E push(E elem);
 
     @StateRefinement(from = "size(this) > 0",
                      to = "size(this) == size(old(this)) - 1",

reference/index.md

@@ -4,27 +4,27 @@ nav_order: 2
 has_children: true
 has_toc: false
 permalink: /reference/
-description: Browse the LiquidJava reference for refinements, typestates, aliases, ghost variables, and external refinements.
+description: Browse the LiquidJava reference for refinements, aliases, state refinements, ghost variables, and external refinements.
 cards:
   - title: Refinements
     url: /reference/refinements/
-    description: Review refinement syntax, annotation forms, and the main rules used during verification.
+    description: Learn about how to use refinements to specify constraints on variables, fields, parameters, and return values.
   - title: Refinement Aliases
     url: /reference/refinement-aliases/
-    description: Reuse common predicates with aliases to keep contracts shorter and easier to maintain.
-  - title: Typestates
-    url: /reference/typestates/
-    description: Model protocol-oriented object states and valid method transitions.
+    description: Learn how to reuse common refinement predicates with aliases to keep contracts shorter and easier to maintain.
+  - title: State Refinements
+    url: /reference/state-refinements/
+    description: Learn how to model protocol-oriented object states and valid method transitions.
   - title: Ghost Variables
     url: /reference/ghost-variables/
-    description: Track logical state that helps express and verify richer object invariants.
+    description: Learn how to track logical state that helps express and verify richer object invariants.
   - title: External Refinements
     url: /reference/external-refinements/
-    description: Attach contracts to code you cannot or do not want to annotate directly.
+    description: Learn how to refine external libraries that cannot be annotated directly.
 ---
 
 # LiquidJava Reference
 
-LiquidJava extends Java with logical refinements and object protocol specifications. This section covers the core annotation model.
+LiquidJava extends Java with logical predicates and object protocol specifications. This section covers the core concepts and features of the LiquidJava type system.
 
 {% include card_grid.html cards=page.cards %}

reference/refinement-aliases.md

@@ -35,4 +35,4 @@ Aliases are a good fit for constraints such as:
 - value classes such as positive or non-negative integers
 - project-wide concepts that appear in many files
 
-For object protocols, move on to [Typestates]({{ '/reference/typestates/' | relative_url }}).
+For object protocols, move on to [State Refinements]({{ '/reference/state-refinements/' | relative_url }}).

reference/refinements.md

@@ -6,16 +6,12 @@ nav_order: 1
 
 # Refinements
 
-Liquid types extend a language with logical predicates over basic types. They let you restrict the values a variable, parameter, field, or return value can have, which helps catch bugs before the program runs.
+In LiquidJava, refinements allow us to express restrictions as logical predicates over basic types. They let us restrict the values a variable, field, parameter, or return value can have, which helps catch bugs before the program runs.
 
-In LiquidJava, refinements are written with `@Refinement`. The predicate must be a boolean expression that refers to the refined value either by its declared name or by `_`.
-
-These constraints are useful for preventing errors such as array index out-of-bounds or division by zero at compile time.
-
-## Variables, Fields, Parameters, and Returns
+These are written as strings in the `@Refinement` annotation. The predicate must be a boolean expression that refers to the refined value either by its declared name or by `_`.
 
 ```java
-import liquidjava.specification.Refinement;
+import liquidjava.specification.*;
 
 public class RefinementExamples {
     @Refinement("x > 0") // x must be greater than 0
@@ -24,42 +20,14 @@ public class RefinementExamples {
     @Refinement("0 <= _ && _ <= 100") // y must be between 0 and 100
     int y;
 
-    @Refinement(value = "z % 2 == 0 ? z >= 0 : z < 0",
-                msg = "z must be positive if even, negative if odd")
+    @Refinement("z % 2 == 0 ? z >= 0 : z < 0") // z must be positive if even, negative if odd
     int z;
 
-    @Refinement("_ >= 0")
-    int absDiv(int a, @Refinement(value = "b != 0", msg = "cannot divide by zero") int b) {
+    @Refinement("_ >= 0") // the return value must be non-negative
+    int absDiv(int a, @Refinement("b != 0") int b) { // b must be non-zero
         int res = a / b;
         return res >= 0 ? res : -res;
     }
 }
 ```
 
-A refinement can be attached to:
-
-- local variables and fields
-- method parameters
-- method return values
-
-## Writing Predicates
-
-Predicates can:
-
-- use the declared variable name directly, such as `x > 0`
-- use `_` as a placeholder for the refined value
-- combine arithmetic, comparisons, conjunctions, disjunctions, and conditional expressions
-- include a custom `msg` to make verification failures easier to understand
-
-## Typical Uses
-
-- Non-zero divisors
-- Positive counters
-- Bounded percentages
-- Numeric relationships between parameters and return values
-
-## What Happens on Failure
-
-When LiquidJava cannot prove a refinement, it reports a verification error at compile time instead of letting the incorrect use reach runtime.
-
-Continue with [Refinement Aliases]({{ '/reference/refinement-aliases/' | relative_url }}) when you want reusable predicate building blocks.

reference/typestates.md reference/state-refinements.mdreference/typestates.md renamed to reference/state-refinements.md

@@ -1,10 +1,10 @@
 ---
-title: Typestates
+title: State Refinements
 parent: Reference
 nav_order: 3
 ---
 
-# Typestates
+# State Refinements
 
 Beyond basic refinements, LiquidJava supports object state modeling through typestates. This lets you describe when a method can or cannot be called based on the state of the object.
 

tooling/cli.md

@@ -35,7 +35,7 @@ mvn exec:java -pl liquidjava-verifier \
 ## Example Outcomes
 
 - A correct file should pass verification.
-- A file that violates a refinement or typestate should produce an error that points to the failed contract.
+- A file that violates a refinement should produce an error that points to the failed contract.
 
 ## When to Use the CLI