Add Diagnostic Sections

Author: rcosta358

_sass/custom/custom.scss

@@ -45,6 +45,18 @@
   box-shadow: 0 18px 36px rgba(15, 23, 42, 0.18);
 }
 
+.main-content .diagnostic-image {
+  display: block;
+  width: 100%;
+  max-width: 100%;
+  margin: 1rem 0 1.5rem;
+  overflow: hidden;
+  border: 1px solid rgba(38, 48, 68, 0.45);
+  border-radius: 1rem;
+  background: linear-gradient(180deg, #172033 0%, #111827 100%);
+  box-shadow: 0 18px 36px rgba(15, 23, 42, 0.18);
+}
+
 .main-content pre,
 .main-content pre.highlight code,
 .main-content div.highlighter-rouge pre,

assets/images/error-message.png

@@ -0,0 +1,27 @@
+---
+title: Custom Messages
+parent: Diagnostics
+nav_order: 3
+---
+
+# Custom Messages
+
+A custom message can be provided to any `@Refinement` or `@StateRefinement` annotation using the `msg` parameter. This message will be  included in the diagnostic when a violation of that annotation is reported, to provide a clearer explanation of the API rule that was violated.
+
+```java
+import liquidjava.specification.*;
+
+@StateSet({"open", "closed"})
+public class MyFile {
+    @StateRefinement(to="open()")
+    public MyFile() {}
+
+    @StateRefinement(from="open()", msg="file must be open to read")
+    public void read(@Refinement(value="_ > 0", msg="bytes must be greater than zero") int bytes) {}
+
+    @StateRefinement(from="open()", to="closed()", msg="file must be open to close")
+    public void close() {}
+}
+```
+
+This is useful to explain the API rule in domain terms for users to quickly understand what went wrong.

diagnostics/custom-messages.md

@@ -0,0 +1,23 @@
+---
+title: Errors
+parent: Diagnostics
+nav_order: 1
+---
+
+# Errors
+
+An error can be caused by a refinement violation, an invalid refinement, or another particular issue.
+
+| Error | Meaning |
+| --- | --- |
+| `RefinementError` | A refinement was violated |
+| `StateRefinementError` | A state refinement was violated |
+| `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 |
+| `StateConflictError` | A state refinement becomes unsatisfiable because it combines disjoint states |
+| `IllegalConstructorTransitionError` | A constructor state refinement declares an illegal `from` transition |
+| `InvalidRefinementError` | A refinement is semantically invalid, such as a non-boolean expression |
+| `CustomError` | Any other error, such as providing a non-existent path to verify |
+
+LiquidJava is only able to report **at most one error per method** to avoid cascading failures. If there are multiple errors in a method, the verifier will report the first one it encounters, and stop verifying the rest of the method, meaning that fixing one error can sometimes reveal another that was previously hidden. 

diagnostics/errors.md

@@ -0,0 +1,27 @@
+---
+title: Diagnostics
+nav_order: 3
+has_children: true
+has_toc: false
+permalink: /diagnostics/
+description: Understand LiquidJava errors, warnings, diagnostic structure, and custom diagnostic messages.
+cards:
+  - title: Errors
+    url: /diagnostics/errors/
+    description: Learn about the different verification errors LiquidJava can report and what each one means.
+  - title: Warnings
+    url: /diagnostics/warnings/
+    description: Learn about the different verification warnings LiquidJava can report and what each one means.
+  - title: Structure
+    url: /diagnostics/structure/
+    description: Learn how to understand a diagnostic message.
+  - title: Custom Messages
+    url: /diagnostics/custom-messages/
+    description: Learn how to provide clearer diagnostic messages using the `msg` parameter.
+---
+
+# Diagnostics
+
+Learn how to understand LiquidJava diagnostics, from verification errors and warnings to the structure of a full diagnostic message.
+
+{% include card_grid.html cards=page.cards %}

diagnostics/index.md

@@ -0,0 +1,52 @@
+---
+title: Diagnostic Structure
+parent: Diagnostics
+nav_order: 4
+---
+
+# Diagnostic Structure
+
+Consider the following refinement error:
+
+![Example LiquidJava refinement error]({{ '/assets/images/error-message.png' | relative_url }})
+{: .diagnostic-image }
+
+Each part gives a different piece of information:
+
+| Part | Meaning |
+| --- | --- |
+| `Refinement Error` | The kind of diagnostic being reported |
+| `#ret² == x / 2 && x > 0` | What LiquidJava knows at the return site. Here, the returned value is `x / 2`, and the parameter refinement says `x > 0` |
+| `is not a subtype of` | LiquidJava is checking whether the inferred refinement is strong enough to satisfy the declared one |
+| `#ret² > 0` | The declared return refinement, obtained from `@Refinement(value="_ > 0", ...)`. |
+| Source snippet | The surrounding lines help locate the failing code in context |
+| Caret line | The `^` marks the exact expression that caused the violation |
+| `result must be positive` | The custom error message from the annotation's `msg` parameter |
+| `Counterexample: x == 1 && #ret² == 0` | A concrete model showing why the check fails. Here we can see the failure arises because if `x == 1`, then `x / 2 == 0` |
+
+## Understanding the Counterexample
+
+The counterexample is a concrete assignment of values that makes the verification fail.
+
+In the example above:
+- `x == 1` satisfies the parameter refinement `x > 0`
+- `#ret² == 0` follows from the return expression `x / 2`, since integer division makes `1 / 2 == 0`
+- `0 > 0` is false, so the declared return refinement is violated
+
+So the counterexample explains exactly why LiquidJava cannot prove that `x / 2` is always positive even when `x > 0`. To fix this error, we would need to either change the return expression to allow to return zero with the refinement `_ >= 0`, or strengthen the parameter refinement to require `x > 1`.
+
+## Internal Instance Variables
+
+Names such as `#ret²` are internal variables introduced by LiquidJava during verification. The small superscript number is a counter used to keep those generated variables unique.
+
+LiquidJava converts expressions into an internal A-normal form (ANF) before verification. Every time it creates a fresh internal variable during that process, the counter is incremented. This is why you may see names such as `#ret²` in the diagnostics.
+
+In practice, you can read `#ret²` as "the internal variable that represents this return value occurrence".
+
+```java
+int example(int x) { // x⁰
+   x = x + 1; // x¹ == x⁰ + 1
+   int y = x / 2; // y² == x¹ / 2
+   return y; // #ret³ == y²
+}
+```

diagnostics/structure.md

@@ -0,0 +1,15 @@
+---
+title: Warnings
+parent: Diagnostics
+nav_order: 2
+---
+
+# Warnings
+
+Warnings do not affect the verification like errors, but they indicate that there is an issue that should probably be addressed.
+
+| Warning | Meaning |
+| --- | --- |
+| `ExternalClassNotFoundWarning` | A class referenced by an external refinement cannot be found |
+| `ExternalMethodNotFoundWarning` | A method referenced by an external refinement cannot be found in the target class |
+| `CustomWarning` | Any other warning, such as reporting that Java compilation errors are present in the program |