Improvements

Author: rcosta358

pages/diagnostics/index.md

@@ -4,9 +4,9 @@ nav_order: 3
 has_children: true
 has_toc: false
 permalink: /diagnostics/
-description: Understand LiquidJava errors and warnings.
+description: Learn about the different types of errors and warnings, how to use custom error messages, and how to interpret refinement errors.
 ---
 
 # Diagnostics
 
-Learn how to understand LiquidJava errors and warnings.
+In this section, you can learn about the different types of errors and warnings that LiquidJava can report, how to use custom error messages to provide more informative feedback, and how to interpret refinement errors.

pages/examples/pagination.md

@@ -15,6 +15,7 @@ import liquidjava.specification.*;
 
 @RefinementAlias("Page(int p) { p >= 1 }")
 @RefinementAlias("PageSize(int s) { 1 <= s && s <= 100 }")
+@RefinementAlias("PageCount(int p) { p >= 0 }")
 @RefinementAlias("ItemCount(int n) { n >= 0 }")
 public class Pagination {
     @Refinement("ItemCount(_) && _ == (page - 1) * size")
@@ -30,7 +31,7 @@ public class Pagination {
         return page + 1;
     }
 
-    @Refinement("Page(_) && _ == (items + size - 1) / size")
+    @Refinement("PageCount(_) && _ == (items + size - 1) / size")
     public static int totalPages(
         @Refinement("ItemCount(_)") int items,
         @Refinement("PageSize(_)") int size
@@ -60,4 +61,5 @@ The aliases capture the key domain concepts for pagination:
 
 - `Page` says page numbers start at `1`
 - `PageSize` constrains the accepted page size range
+- `PageCount` prevents negative page counts
 - `ItemCount` prevents negative item counts

pages/examples/reentrant-lock.md

@@ -0,0 +1,40 @@
+---
+title: Semaphore
+parent: Examples
+nav_order: 9
+permalink: /examples/semaphore/
+description: An external typestate refinement for a simple semaphore protocol.
+---
+
+# Semaphore
+
+This example refines `java.util.concurrent.Semaphore` with a simple two-state protocol that models a binary semaphore being acquired and released.
+
+```java
+import liquidjava.specification.*;
+
+@ExternalRefinementsFor("java.util.concurrent.Semaphore")
+@StateSet({"available", "acquired"})
+public interface SemaphoreRefinements {
+    @StateRefinement(to="available()")
+    public void Semaphore(@Refinement("_ == 1") int permits);
+
+    @StateRefinement(from="available()", to="acquired()")
+    public void acquire();
+
+    @StateRefinement(from="acquired()", to="available()")
+    public void release();
+}
+```
+
+```java
+Semaphore semaphore = new Semaphore(1);
+semaphore.acquire();
+semaphore.release();
+semaphore.release(); // State Refinement Error
+```
+
+The external refinement enforces the expected protocol: `acquire()` is only allowed when the semaphore is `available()`, and `release()` is only allowed when it is `acquired()`.
+
+{: .note }
+This specification models a binary semaphore with one permit. It does not account for semaphores with multiple permits or concurrent access across multiple threads.