Add Pagination and Slice Range Examples

Author: rcosta358

pages/examples/arraylist.md

@@ -1,7 +1,7 @@
 ---
 title: ArrayList
 parent: Examples
-nav_order: 7
+nav_order: 9
 permalink: /examples/arraylist/
 description: An external refinement for ArrayList that prevents out-of-bounds access.
 ---

pages/examples/connection.md

@@ -1,7 +1,7 @@
 ---
 title: Connection
 parent: Examples
-nav_order: 6
+nav_order: 8
 permalink: /examples/connection/
 description: A typestate protocol with a value-dependent conditional transition.
 ---

pages/examples/downloader.md

@@ -1,7 +1,7 @@
 ---
 title: Downloader
 parent: Examples
-nav_order: 5
+nav_order: 7
 permalink: /examples/downloader/
 description: A typestate protocol for a downloader object.
 ---

pages/examples/email.md

@@ -1,7 +1,7 @@
 ---
 title: Email
 parent: Examples
-nav_order: 3
+nav_order: 5
 permalink: /examples/email/
 description: A typestate protocol for a Email builder API.
 ---

pages/examples/media-player.md

@@ -1,7 +1,7 @@
 ---
 title: Media Player
 parent: Examples
-nav_order: 2
+nav_order: 4
 permalink: /examples/media-player/
 description: A typestate protocol for a simple media player.
 ---

pages/examples/order.md

@@ -1,7 +1,7 @@
 ---
 title: Order
 parent: Examples
-nav_order: 4
+nav_order: 6
 permalink: /examples/order/
 description: A typestate protocol for a simple order processing system.
 ---

pages/examples/pagination.md

@@ -0,0 +1,63 @@
+---
+title: Pagination
+parent: Examples
+nav_order: 2
+permalink: /examples/pagination/
+description: Plain refinements with aliases for page numbers, page sizes, and computed offsets.
+---
+
+# Pagination
+
+This example uses plain refinements and refinement aliases to describe common pagination rules. The aliases keep the contracts readable while still relating results to the input values.
+
+```java
+import liquidjava.specification.*;
+
+@RefinementAlias("Page(int p) { p >= 1 }")
+@RefinementAlias("PageSize(int s) { 1 <= s && s <= 100 }")
+@RefinementAlias("ItemCount(int n) { n >= 0 }")
+public class Pagination {
+    @Refinement("ItemCount(_) && _ == (page - 1) * size")
+    public static int offset(
+        @Refinement("Page(_)") int page,
+        @Refinement("PageSize(_)") int size
+    ) {
+        return (page - 1) * size;
+    }
+
+    @Refinement("Page(_) && _ == page + 1")
+    public static int nextPage(@Refinement("Page(_)") int page) {
+        return page + 1;
+    }
+
+    @Refinement("Page(_) && _ == (items + size - 1) / size")
+    public static int totalPages(
+        @Refinement("_ > 0") int items,
+        @Refinement("PageSize(_)") int size
+    ) {
+        return (items + size - 1) / size;
+    }
+}
+```
+
+```java
+int size = 20;
+int page = 3;
+int offset = Pagination.offset(page, size);
+int next = Pagination.nextPage(page);
+int total = Pagination.totalPages(50, size);
+```
+
+```java
+Pagination.offset(0, 20); // Refinement Error
+```
+
+```java
+Pagination.totalPages(50, 200); // Refinement Error
+```
+
+The aliases capture the key domain concepts for pagination:
+
+- `Page` says page numbers start at `1`
+- `PageSize` constrains the accepted page size range
+- `ItemCount` marks non-negative counts such as offsets

pages/examples/reentrant-lock.md

@@ -1,7 +1,7 @@
 ---
 title: ReentrantLock
 parent: Examples
-nav_order: 7
+nav_order: 10
 permalink: /examples/reentrant-lock/
 description: An external typestate refinement for ReentrantLock.
 ---

pages/examples/slice-range.md

@@ -0,0 +1,62 @@
+---
+title: Slice Range
+parent: Examples
+nav_order: 3
+permalink: /examples/slice-range/
+description: Plain refinements with aliases for valid index ranges and slice lengths.
+---
+
+# Slice Range
+
+This example models a small utility for working with array slices. It uses plain refinements and aliases with multiple parameters to encode reusable range checks.
+
+```java
+import liquidjava.specification.*;
+
+@RefinementAlias("Length(int n) { n >= 0 }")
+@RefinementAlias("ValidIndex(int i, int size) { 0 <= i && i < size }")
+@RefinementAlias("ValidRange(int start, int end, int size) { 0 <= start && start <= end && end <= size }")
+public class SliceRange {
+    @Refinement("Length(_) && _ == end - start")
+    public static int sliceLength(
+        @Refinement("Length(size)") int size,
+        int start,
+        @Refinement("ValidRange(start, end, size)") int end
+    ) {
+        return end - start;
+    }
+
+    @Refinement("ValidIndex(_, size)")
+    public static int lastIndex(@Refinement("size > 0") int size) {
+        return size - 1;
+    }
+
+    @Refinement("Length(_) && _ == index + 1")
+    public static int prefixLength(
+        @Refinement("Length(size)") int size,
+        @Refinement("ValidIndex(index, size)") int index
+    ) {
+        return index + 1;
+    }
+}
+```
+
+```java
+int size = 10;
+int part = SliceRange.sliceLength(size, 2, 6);
+int last = SliceRange.lastIndex(size);
+int prefix = SliceRange.prefixLength(size, 4);
+```
+
+```java
+SliceRange.sliceLength(10, 7, 3); // Refinement Error
+```
+
+```java
+SliceRange.prefixLength(10, 10); // Refinement Error
+```
+
+The aliases capture the key domain concepts for working with slices:
+- `Length` says lengths are non-negative
+- `ValidIndex` says an index is valid if it is within the bounds of the size
+- `ValidRange` says a range is valid if it starts and ends within the bounds of the size, and the start is not after the end