Document verification features with checked Java examples (#2)

Author: rcosta358

pages/command-line-interface.md

@@ -1,6 +1,6 @@
 ---
 title: Command-Line Interface
-nav_order: 5
+nav_order: 6
 permalink: /command-line-interface/
 description: Run the LiquidJava verifier from the command line for local checks, debugging, and CI workflows.
 ---

pages/diagnostics/index.md

@@ -1,6 +1,6 @@
 ---
 title: Diagnostics
-nav_order: 3
+nav_order: 4
 has_children: true
 has_toc: false
 permalink: /diagnostics/

pages/examples/index.md

@@ -1,6 +1,6 @@
 ---
 title: Examples
-nav_order: 6
+nav_order: 7
 has_children: true
 permalink: /examples/
 description: LiquidJava example usages with focused code snippets.

pages/resources.md

@@ -1,6 +1,6 @@
 ---
 title: Resources
-nav_order: 7
+nav_order: 8
 has_children: false
 permalink: /resources/
 description: Find LiquidJava papers, posters, and source repositories for deeper reading and experimentation.

pages/verification/conditionals.md

@@ -0,0 +1,53 @@
+---
+title: Conditionals
+parent: Verification Features
+nav_order: 2
+permalink: /verification/conditionals/
+description: Learn how if and else conditions provide facts for refinement checks.
+---
+
+# Conditionals
+
+An `if` condition adds information along each branch. The `then` branch is checked assuming the condition is true; the `else` branch is checked assuming it is false.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class ConditionalExample {
+    public static void requirePositive(
+            @Refinement("_ > 0") int value) {}
+    public static void requireNonPositive(
+            @Refinement("_ <= 0") int value) {}
+
+    public static void guarded(int value) {
+        if (value > 0) {
+            requirePositive(value); // accepted: value > 0
+        } else {
+            requireNonPositive(value); // accepted: value <= 0
+        }
+    }
+}
+```
+
+Although `guarded` accepts any integer, each call is protected by a condition that establishes the required refinement. No extra refinement on its parameter is needed for these calls.
+
+## The Condition Must Be Strong Enough
+
+Changing the guard to `value >= 0` does not prove strict positivity, because zero remains possible:
+
+```java
+import liquidjava.specification.Refinement;
+
+public class WeakGuardExample {
+    public static void requirePositive(
+            @Refinement("_ > 0") int value) {}
+
+    public static void guarded(int value) {
+        if (value >= 0) {
+            requirePositive(value); // Refinement Error: value could be 0
+        }
+    }
+}
+```
+
+Branch assumptions apply to the paths on which they hold. After an `if`/`else` where both branches continue, code must work for either outcome; it cannot assume that the `then` condition is still true. Nested conditions can provide additional facts inside their branches.

pages/verification/index.md

@@ -0,0 +1,36 @@
+---
+title: Verification Features
+nav_order: 3
+has_children: true
+has_toc: false
+permalink: /verification/
+description: Understand how LiquidJava checks assignments, method calls, conditionals, and recursive methods.
+---
+
+# Verification Features
+
+The [Annotations]({{ '/annotations/' | relative_url }}) section explains how to write specifications. This section explains how LiquidJava uses them when checking Java code, without running the program.
+
+At a check, the verifier gathers facts about the values in scope and asks an SMT solver whether those facts imply the required refinement. For example, knowing `x == 5` is enough to prove `x > 0`. Knowing only `x >= 0` is not: `x` could be zero.
+
+## Variables and Assignments
+
+A local variable's initializer must satisfy its declared refinement. Later assignments must satisfy that same refinement, even when the value changes.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class AssignmentExample {
+    public static void example() {
+        @Refinement("_ > 0") int count = 1;
+        count = 2; // accepted: 2 > 0
+        count = 0; // Refinement Error: 0 is not positive
+    }
+}
+```
+
+The verifier also tracks information from expressions and assignments. An unannotated local such as `int count = 1` can therefore carry useful information; it does not declare a requirement that every later value must equal `1`.
+
+## When a Check Fails
+
+A refinement error means the verifier could not establish the required predicate from the available facts. The code may violate the requirement, or the verifier may need a stronger parameter refinement, a branch condition, or a return contract to establish it. See [Understanding Refinement Errors]({{ '/diagnostics/understanding-refinement-errors/' | relative_url }}) for interpreting the diagnostic and its counterexample.

pages/verification/method-calls.md

@@ -0,0 +1,54 @@
+---
+title: Method Calls and Returns
+parent: Verification Features
+nav_order: 1
+permalink: /verification/method-calls/
+description: Learn how parameter and return refinements connect a method's implementation to its callers.
+---
+
+# Method Calls and Returns
+
+A method contract has two sides:
+
+- **Parameters:** callers must establish each parameter's refinement. The method body can assume those refinements.
+- **Return value:** each return must satisfy the method's declared refinement. Callers can use that refinement for the result.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class MethodExample {
+    @Refinement("_ == value")
+    public static int positiveIdentity(
+            @Refinement("value > 0") int value) {
+        return value;
+    }
+
+    public static void example() {
+        @Refinement("_ == 3") int result = positiveIdentity(3);
+        positiveIdentity(0); // Refinement Error: 0 is not positive
+    }
+}
+```
+
+For `positiveIdentity(3)`, the verifier checks `3 > 0`. It then substitutes the argument into the return contract `_ == value`, so the result is known to equal `3`. The call with `0` fails the parameter check.
+
+The body is checked separately using its parameter contract. Returning a value that contradicts its return contract also produces an error:
+
+```java
+import liquidjava.specification.Refinement;
+
+public class ReturnExample {
+    @Refinement("_ > 0")
+    public static int positive() {
+        return 0; // Refinement Error: 0 is not positive
+    }
+}
+```
+
+Write the return properties callers need explicitly. For example, without a return refinement on `positiveIdentity`, callers should not rely on the verifier inspecting its body to discover that the result equals the argument.
+
+## Object State at a Call
+
+For a method with [state refinements]({{ '/annotations/state-refinement/' | relative_url }}), the verifier also checks that the receiver satisfies `from` before the call and uses `to` to describe its state afterward. A constructor's `to` establishes the initial state. This is how a protocol can reject a `read()` call after `close()`.
+
+For library methods whose source is outside the checked code, use [external refinements]({{ '/annotations/external-refinements-for/' | relative_url }}) to supply contracts. Those contracts describe the library behavior the verifier relies on; they do not verify the library's implementation.

pages/verification/recursion.md

@@ -0,0 +1,57 @@
+---
+title: Recursion
+parent: Verification Features
+nav_order: 3
+permalink: /verification/recursion/
+description: Learn how LiquidJava checks recursive calls using parameter and return refinements.
+---
+
+# Recursion
+
+A recursive call is checked using the same parameter and return refinements as any other method call. LiquidJava uses the declared contract instead of repeatedly expanding the method body.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class RecursionExample {
+    @Refinement("_ == 0")
+    public static int untilZero(
+            @Refinement("k >= 0") int k) {
+        if (k == 0) {
+            return 0;
+        } else {
+            return untilZero(k - 1);
+        }
+    }
+}
+```
+
+The verifier checks both branches:
+
+1. In the base case, returning `0` satisfies `_ == 0`.
+2. In the other branch, `k >= 0` and `k != 0` imply `k > 0`, since `k` is an integer. Therefore `k - 1 >= 0`, so the recursive call satisfies the parameter contract.
+3. The recursive call's return contract says its result equals `0`, which satisfies the enclosing method's return contract.
+
+## An Incorrect Base Case
+
+If the base case tests `k == 1`, the other branch can include `k == 0`. Subtracting one then violates the recursive call's parameter refinement:
+
+```java
+import liquidjava.specification.Refinement;
+
+public class IncorrectRecursionExample {
+    @Refinement("_ == 0")
+    public static int untilZero(
+            @Refinement("k >= 0") int k) {
+        if (k == 1) {
+            return 0;
+        } else {
+            // k could be 0, so k - 1 could be negative
+            return untilZero(k - 1); // Refinement Error
+        }
+    }
+}
+```
+
+{: .note }
+Checking recursive contracts does not prove termination or bound recursion depth. An accepted recursive method can still recurse forever or exhaust the Java stack. The return refinement describes the value if the method returns.

pages/vscode-extension/index.md

@@ -1,6 +1,6 @@
 ---
 title: VS Code Extension
-nav_order: 4
+nav_order: 5
 has_children: true
 has_toc: false
 permalink: /vscode-extension/