LSP server for OpenJML

OpenJML

OpenJML, the tool implementing the Java Modeling Language, is a command-line tool that also implements a standard Language Server Protocol (LSP) interface that enables language support for JML with any LSP-supporting IDE.

The OpenJML LSP implements the following standard LSP features. See the subpages on individual IDEs for descriptions of how the OpenJML functionality is enabled in each IDE.

  • Displaying OpenJML warnings and errors as standard markers in file editor windows
  • Syntax coloring -- coloring JML text in an editor window according to the kinds of parser tokens
  • Go to Definition -- navigating from an identifier to its declaration
  • Find References -- finding all uses of a given identifier across the project
  • Document highlights -- highlighting all occurrences of an identifier in the current file
  • Rename -- renaming all instances of a given identifier
  • Workspace symbol search -- finding declarations by name across all checked files
  • Outline -- showing JML and Java declarations in the file outline (configurable: JML-only or combined)
  • Hover -- showing the JML specification of the method under the cursor
  • Code completion -- of JML keywords in JML contexts
  • Folding of multi-line JML text
  • Code lens information near method declarations showing OpenJML verification status (Verified, Not verified, Type errors, etc.); appears after the first check completes
  • An Output pane showing progress information from the LSP server and underlying OpenJML
  • Signature help -- shows method signature types and formal parameter names as you type
  • Inlay hints -- showing the inferred type of var-declared variables in both Java and JML contexts

The OpenJML LSP also implements a number of actions, typically implemented as GUI menu options or buttons:

  • Parsing/typechecking triggered by edits, saves, or explicit request (configurable)
  • Run static checking (ESC) on folders, files, or methods
  • Cancel currently running ESC proof attempts
  • Compile a file with runtime-assertion checking

There are a number of options controlling OpenJML that are implemented as Settings or Preferences in the various IDEs, including when type-checking and ESC run automatically (on edit, on save, or manually only). For many of these settings there are defaults that are appropriate for most work. Though the OpenJML language server is implemented to be sufficient for a generic client, the OpenJML project has also implemented some specific clients: