Improve Wording

Author: rcosta358

reference/external-refinements.md

@@ -6,9 +6,9 @@ nav_order: 4
 
 # External Refinements
 
-External refinements let us add refinements to an existing class that we cannot modify.
+External refinements let you add refinements to an existing class that you cannot modify.
 
-For this, we use the `@ExternalRefinementsFor` annotation to specify the qualified name of the class we want to refine in a separate interface. This lets us refine external classes from the Java standard library, third-party dependencies, or shared APIs without modifying their source code.
+For this, the `@ExternalRefinementsFor` annotation is used to specify the qualified name of the class you want to refine in a separate interface. This makes it possible to refine external classes from the Java standard library, third-party dependencies, or shared APIs without modifying their source code.
 
 ```java
 import liquidjava.specification.*;

reference/refinement-aliases.md

@@ -6,7 +6,7 @@ nav_order: 2
 
 # Refinement Aliases
 
-When the same refinement appears repeatedly, we can define it once with `@RefinementAlias` and reuse it inside other refinements.
+When the same refinement appears repeatedly, you can define it once with `@RefinementAlias` and reuse it inside other refinements.
 
 ```java
 import liquidjava.specification.*;

reference/refinements.md

@@ -6,7 +6,7 @@ nav_order: 1
 
 # Refinements
 
-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 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.
 
 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 `_`.
 
@@ -33,7 +33,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 we cover 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 is covered in later sections.
 
 | Form | Syntax | Example |
 | --- | --- | --- |

reference/state-refinements.md

@@ -39,7 +39,7 @@ If a class follows an implicit protocol that can be described by a DFA, the prot
 
 ## Syntax
 
-Note that states are functions. These take a single parameter, which is the object being refined. Since we are describing the state of the current object, we use `this` as the parameter, which is being used implicitly in the example above. Actually, all of these are equivalent: `open()`, `this.open()`, and `open(this)`.
+Note that states are functions. These take a single parameter, which is the object being refined, in this case the implicit `this`. All of these are equivalent: `open()`, `this.open()`, and `open(this)`.
 
 ## State Initialization
 
@@ -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 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`.