Add Corrections

Author: rcosta358

pages/404.md

@@ -6,7 +6,7 @@ nav_exclude: true
 
 # Page Not Found
 
-This page you requested does not exist.
+The page you requested does not exist.
 
 - Go back to the [homepage]({{ '/' | relative_url }})
 - Open [Getting Started]({{ '/getting-started/overview/' | relative_url }})

pages/command-line-interface.md

@@ -5,13 +5,13 @@ permalink: /command-line-interface/
 description: Run the LiquidJava verifier from the command line for local checks, debugging, and CI workflows.
 ---
 
-# Command-Line 
+# Command-Line Interface
 
-The LiquidJava verifier can be run from the command line, which the following options:
+The LiquidJava verifier can be run from the command line with the following options:
 
 | Option | Description |
 | --- | --- |
-| `<...paths>` | Paths (file or directories) to be verified by LiquidJava |
+| `<...paths>` | Paths (files or directories) to be verified by LiquidJava |
 | `--help` | Show the help message with available options |
 | `--version` | Show the current version of the verifier |
 | `--debug` | Enable debug logging and skip expression simplification for troubleshooting |

pages/concepts/ghosts.md

@@ -8,7 +8,7 @@ description: Learn how to track logical state that helps express and verify rich
 
 # Ghosts
 
-Some protocols need more than a small set of named states. LiquidJava supports ghost variables for tracking extra state. They can be used in refinements and state refinements to express richer invariants about the object. Similarly to the states, these are functions that take the object being refined as a parameter.
+Some protocols need more than a small set of named states. LiquidJava supports ghost variables for tracking extra state. They can be used in refinements and state refinements to express richer invariants about an object. Like states, ghosts are functions that take the refined object as a parameter.
 
 Ghosts are declared with the `@Ghost` annotation, and they can be updated with `@StateRefinement` annotations on methods.
 
@@ -39,7 +39,7 @@ s.pop();
 s.pop(); // State Refinement Error
 ```
 
-In the "constructor" method, the ghost variable `size` is initialized to 0. An equality in a method postcondition is how ghost variables are updated. However, here it is not necessary, since when no postcondition is declared, it is initialized to its default value, similarly to how Java initializes fields to their default values when no explicit initializer is provided (`int --> 0`, `boolean --> false`, etc.). 
+In the "constructor" method, the ghost variable `size` is initialized to `0`. An equality in a method postcondition is how ghost variables are updated. In this case, the explicit postcondition is optional, because if no postcondition is declared the ghost variable is initialized to its default value, similarly to how Java initializes fields with no explicit initializer (`int -> 0`, `boolean -> false`, and so on).
 
 In the `push` method, we specify no precondition, since we can always push an element to the stack, but we specify a postcondition that increments the `size` by one. In this case, we tell the typechecker that the new value of `size` after calling `push` is equal to the old value of `size` plus one. This is possible using the `old` function, which takes an object instance and returns its value before the method call.
 

pages/concepts/refinements.md

@@ -8,7 +8,7 @@ description: Learn about how to use refinements to specify constraints on variab
 
 # Refinements
 
-In LiquidJava, refinements allow you to express restrictions as logical predicates over basic types. They let you restrict the values a variable, field, parameter, or return value can have, which helps catch bugs before the program runs.
+In LiquidJava, refinements allow you to express restrictions as logical predicates over basic types. They let you restrict the values that a variable, field, parameter, or return value can have, which helps catch bugs before the program runs.
 
 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 `_`.
 
@@ -35,7 +35,7 @@ public class RefinementExamples {
 
 ## Predicate Syntax
 
-Refinement predicates use a language similar to Java, where you can write boolean expressions using comparisons, logical connectives, arithmetic operators, conditional expressions, and calls to ghosts or aliases, which is covered in later sections.
+Refinement predicates use a language similar to Java, where you can write boolean expressions using comparisons, logical connectives, arithmetic operators, conditional expressions, and calls to ghosts or aliases, which are covered in later sections.
 
 | Form | Syntax | Example |
 | --- | --- | --- |

pages/diagnostics/custom-messages.md

@@ -8,7 +8,7 @@ description: Learn how to provide clearer diagnostic messages.
 
 # Custom Messages
 
-A custom message can be provided to any `@Refinement` or `@StateRefinement` annotation using the `msg` parameter. This message will be  included in the diagnostic when a violation of that annotation is reported, to provide a clearer explanation of the API rule that was violated.
+A custom message can be provided to any `@Refinement` or `@StateRefinement` annotation using the `msg` parameter. This message will be included in the diagnostic when a violation of that annotation is reported, providing a clearer explanation of the API rule that was violated.
 
 ```java
 import liquidjava.specification.*;

pages/diagnostics/errors.md

@@ -22,4 +22,4 @@ An error can be caused by a refinement violation, an invalid refinement, or anot
 | `InvalidRefinementError` | A refinement is semantically invalid, such as a non-boolean expression |
 | `CustomError` | Any other error, such as providing a non-existent path to verify |
 
-LiquidJava is only able to report **at most one error per method** to avoid cascading failures. If there are multiple errors in a method, the verifier will report the first one it encounters, and stop verifying the rest of the method, meaning that fixing one error can sometimes reveal another that was previously hidden. 
+LiquidJava is only able to report **at most one error per method** to avoid cascading failures. If there are multiple errors in a method, the verifier will report the first one it encounters and stop verifying the rest of the method. This means that fixing one error can sometimes reveal another that was previously hidden.

pages/diagnostics/understanding-refinement-errors.md

@@ -41,15 +41,15 @@ In the example above:
 - `#ret² == 0` follows from the return expression `x / 2`, since integer division makes `1 / 2 == 0`
 - `0 > 0` is false, so the declared return refinement is violated
 
-So the counterexample explains exactly why LiquidJava cannot prove that `x / 2` is always positive even when `x > 0`. To fix this error, we would need to either weaken the return expression to allow to return zero with the refinement `_ >= 0`, or strengthen the parameter refinement to require `x > 1`.
+So the counterexample explains exactly why LiquidJava cannot prove that `x / 2` is always positive even when `x > 0`. To fix this error, we would need to either weaken the return refinement to allow zero with `_ >= 0`, or strengthen the parameter refinement to require `x > 1`.
 
 ## Internal Variables
 
 Names such as `#ret²` are internal variables created by LiquidJava during verification. The small superscript number is a counter used to keep those generated variables unique.
 
 LiquidJava converts expressions into an internal A-normal form (ANF) before verification. Every time it creates a fresh internal variable during that process, the counter is incremented. This is why you may see names such as `#ret²` in the diagnostics. In practice, you can read `#ret²` as "the internal variable that represents this return value occurrence".
 
-The following example shows how the internal variables are created during the typechecking:
+The following example shows how the internal variables are created in the typechecking:
 
 ```java
 int example(int x) { // x⁰

pages/examples/arraylist.md

@@ -8,7 +8,7 @@ description: An external refinement for ArrayList that prevents out-of-bounds ac
 
 # ArrayList
 
-This example refines the `java.util.ArrayList` standard-library class without modifying its source code. A ghost variable tracks the size of the list, and method refinements to prevent out-of-bounds accesses.
+This example refines the `java.util.ArrayList` standard-library class without modifying its source code. A ghost variable tracks the size of the list, and a parameter refinement prevents out-of-bounds accesses.
 
 ```java
 import liquidjava.specification.*;

pages/examples/downloader.md

@@ -11,6 +11,8 @@ description: A typestate protocol for a downloader object.
 This example models a simple downloader object that tracks the progress of a download operation by combining typestates and ghost variables.
 
 ```java
+import liquidjava.specification.*;
+
 @Ghost("int progress")
 @StateSet({"created", "downloading", "completed"})
 public class Downloader {

pages/examples/email.md

@@ -3,7 +3,7 @@ title: Email
 parent: Examples
 nav_order: 5
 permalink: /examples/email/
-description: A typestate protocol for a Email builder API.
+description: A typestate protocol for an Email builder API.
 ---
 
 # Email
@@ -40,18 +40,18 @@ public class Email {
 
 ```java
 Email email = new Email();
-email.from("me");
-     .to("bob");
-     .to("alice");
-     .subject("greetings");
-     .body("hello!");
+email.from("me")
+     .to("bob")
+     .to("alice")
+     .subject("greetings")
+     .body("hello!")
      .build();
 ```
 
 ```java
 Email email = new Email();
-email.from("me");
-     .to("bob");
+email.from("me")
+     .to("bob")
      .build(); // State Refinement Error
 ```
 
@@ -60,4 +60,4 @@ LiquidJava enforces the intended protocol:
 - The `from` must be set first
 - The `to` must be set at least once before setting the `body`
 - The `subject` is optional
-- The `build` is only allowed to be set after the body
+- The `build` method can only be called after the body is set