Improvements

Author: rcosta358

concepts/refinements.md

@@ -45,5 +45,5 @@ Refinement predicates use a language similar to Java, where you can write boolea
 | Literals | `true` `false` `0` `1.5` | `@Refinement("_ == true") boolean ok = true;` |
 
 LiquidJava currently only supports a small set of types in refinements:
-- Primitive types: `int`, `boolean`, `long`, `double`, `float`
-- Boxed types: `Boolean`, `Integer`, `Double`
+- The primitive types `int` `boolean` `long` `double` `float`
+- The boxed types `Boolean` `Integer` `Double`

concepts/state-refinements.md

@@ -8,9 +8,9 @@ nav_order: 3
 
 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.
 
-The possible states of a class are declared with `@StateSet`, and the state transitions are described with `@StateRefinement(from = "...", to = "...")`:
-- `from` describes the **precondition** - the object state in which the method can be invoked
-- `to` describes the **postcondition** - the state the object will have after the method is called
+The possible states of a class are declared with `@StateSet`, and the state transitions are described with `@StateRefinement(from="...", to="...")`.
+- The `from` describes the **precondition** - the object state in which the method can be invoked
+- The `to` describes the **postcondition** - the state the object will have after the method is called
 
 ```java
 import liquidjava.specification.*;
@@ -55,7 +55,7 @@ public class Buffer {
 }
 ```
 
-If no `to` transition is written, LiquidJava defaults the constructor to the first state listed in the corresponding `@StateSet`.
+If no `to` transition is declared, LiquidJava defaults the constructor to the first state listed in the corresponding `@StateSet`.
 
 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.
 
@@ -88,4 +88,4 @@ public class Device {
 
 Each state set is exclusive: at any moment, the object can only be in one state from that specific set. In the example above, the object cannot be both `open` and `closed`, and it cannot be both `clean` and `dirty`.
 
-When a transition affects multiple orthogonal states, the states must be combined with `&&` in the `from` and `to` annotations. In the example above, the `use` method transitions from `open && clean` to `open && dirty`, and the `close` method transitions from `open && clean` to `closed && clean`.
+When using more than one state set, the states must be combined with `&&` in the `from` and `to` annotations, as shown in the example above. This is because the object must always be in exactly one state from each set, so we need to specify the full state of the object in the preconditions and postconditions.

getting-started/index.md

@@ -6,12 +6,12 @@ has_toc: false
 permalink: /getting-started/
 description: Start with the LiquidJava basics, from overview to setup and a first verification run.
 cards:
-  - title: Overview
-    url: /getting-started/overview/
-    description: Learn what LiquidJava adds to Java.
   - title: Setup
     url: /getting-started/setup/
     description: Set up the dependency, verifier, and VS Code extension to start using LiquidJava.
+  - title: Overview
+    url: /getting-started/overview/
+    description: Learn what LiquidJava adds to Java.
 ---
 
 # Getting Started