Update Understanding Refinement Errors Section

Author: rcosta358

diagnostics/index.md

@@ -4,7 +4,7 @@ nav_order: 3
 has_children: true
 has_toc: false
 permalink: /diagnostics/
-description: Understand LiquidJava errors, warnings, diagnostic structure, and custom diagnostic messages.
+description: Understand LiquidJava errors and warnings.
 cards:
   - title: Errors
     url: /diagnostics/errors/
@@ -15,13 +15,13 @@ cards:
   - title: Custom Messages
     url: /diagnostics/custom-messages/
     description: Learn how to provide clearer diagnostic messages using the `msg` parameter.
-  - title: Diagnostic Structure
-    url: /diagnostics/diagnostic-structure/
-    description: Learn how to understand a diagnostic message.
+  - title: Understanding Refinement Errors
+    url: /diagnostics/understanding-refinement-errors/
+    description: Learn how to read and interpret LiquidJava refinement errors.
 ---
 
 # Diagnostics
 
-Learn how to understand LiquidJava diagnostics, from verification errors and warnings to the structure of a full diagnostic message.
+Learn how to understand LiquidJava errors and warnings.
 
 {% include card_grid.html cards=page.cards %}

diagnostics/diagnostic-structure.md …stics/understanding-refinement-errors.mddiagnostics/diagnostic-structure.md renamed to diagnostics/understanding-refinement-errors.md diagnostics/diagnostic-structure.md renamed to diagnostics/understanding-refinement-errors.md

@@ -1,10 +1,10 @@
 ---
-title: Diagnostic Structure
+title: Understanding Refinement Errors
 parent: Diagnostics
 nav_order: 4
 ---
 
-# Diagnostic Structure
+# Understanding Refinement Errors
 
 Consider the following refinement error:
 
@@ -26,7 +26,11 @@ Each part gives a different piece of information:
 
 The error message also includes the absolute path of the file and line where the error was reported, which can be clicked to jump the source code location in the editor.
 
-## Understanding the Error
+## Subtyping
+
+To verify if a refinement holds, LiquidJava checks if the inferred refinement is a subtype of the expected one. This means that every value that satisfies the inferred refinement must also satisfy the expected one. For example, the predicate `x > 0` is a subtype of `x >= 0`, since the set of positive integers is contained within the set of non-negative integers. However, `x > 0` is not a subtype of `x > 1`, since the value `x == 1` satisfies the first predicate but not the second.
+
+## Counterexamples
 
 Refinement errors may provide a counterexample, which is a concrete assignment of values that makes the verification fail.
 

index.md

@@ -13,7 +13,7 @@ cards:
     description: Look up LiquidJava concepts, annotations, and protocol rules in a more formal, detailed format.
   - title: Diagnostics
     url: /diagnostics/
-    description: Understand LiquidJava errors, warnings, diagnostic structure, and custom diagnostic messages.
+    description: Understand LiquidJava errors and warnings.
   - title: VS Code Extension
     url: /vscode/
     description: Find out about real-time diagnostics, syntax highlighting, and more in the editor.