Diagnostic Explorer

The diagnostic explorer provides an interactive view of LiquidJava diagnostics with extra information not available in the command-line interface.

For refinement errors, LiquidJava performs expression simplification with traceable simplification steps. This makes it possible to progressively expand simplifications. Clicking a value can expand it into its origin expression, and clicking a variable can jump to its location in the editor. This makes simplification traceable instead of showing only the final reduced expression.

In refinement and state refinement errors, an expandable section displays the context variables (also called translation table). This table maps the internal variable names created during the typechecking to the original source code variables and placement in the code. When clicked, each entry highlights the corresponding part of the source code that corresponds to that variable.