Fixes

Author: rcosta358

pages/diagnostics/errors.md

@@ -12,8 +12,8 @@ An error can be caused by a refinement violation, an invalid refinement, or anot
 
 | Error | Meaning |
 | --- | --- |
-| `RefinementError` | A refinement was violated |
-| `StateRefinementError` | A state refinement was violated |
+| `RefinementError` | A refinement was violated or could not be proven |
+| `StateRefinementError` | A state refinement was violated or could not be proven |
 | `NotFoundError` | An element used in a refinement could not be found |
 | `SyntaxError` | The syntax used in a refinement is invalid |
 | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments |

pages/examples/arraylist.md

@@ -21,7 +21,7 @@ public interface ArrayListRefinements<E> {
     @StateRefinement(to="size() == size(old(this)) + 1")
     public boolean add(E elem);
 
-    public E get(@Refinement("_ < size()") int index);
+    public E get(@Refinement("0 <= _ && _ < size()") int index);
 }
 ```
 

pages/examples/pagination.md

@@ -32,7 +32,7 @@ public class Pagination {
 
     @Refinement("Page(_) && _ == (items + size - 1) / size")
     public static int totalPages(
-        @Refinement("_ > 0") int items,
+        @Refinement("ItemCount(_)") int items,
         @Refinement("PageSize(_)") int size
     ) {
         return (items + size - 1) / size;
@@ -60,4 +60,4 @@ 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
+- `ItemCount` prevents negative item counts