VDM Language Support in Visual Studio Code

VDM-VSCode is an extension for Visual Studio Code (VS Code) that provides language support for the VDM dialects VDM-SL, VDM++ and VDM-RT. The extension utilises a language server powered by VDMJ that is developed by Nick Battle.

Installation

In Visual Studio Code just type @id:jonaskrask.vdm-vscode in the Extensions view Search box or type vdm and select VDM VSCode.

Requirements

• Visual Studio Code ≥ v. 1.49.0
• Java ≥ v. 11

Features

• Syntax Highlighting
• Syntax- and type-checking
• Smart navigation
• Debugging
• Proof Obligation Generation
• Combinatiorial Testing
• Translation to LaTeX and Word
• Java code generation
• Dependency graph generation
• Coverage report
• Import of project examples
• Import of VDM libraries

Future Work

• Improve syntax highlighting
• Improve debugging execution
• Show all workspace folders in the Combinatorial Testing view

Usage

Open a folder (single VDM project) or a workspace (multiple VDM projects) and then open a VDM file(.vdmsl, .vdmpp or .vdmrt) in from the explorer window. This will automatically start language server in the background. The following displays snippets of the feature functionalities provided by the extension and their use:

• Syntax highlighting: VDM keywords are automatically highlighted.
  
  

• Syntax- and type-checking: Syntax- and type-errors and warnings are highligthed in the editor and detailed in the terminal or by hovering on the highlighted section.
  
  

• Smart navigation: Mutiple actions exists for navigating to the definition of a given identifier in a specification: Ctrl + click, the right-click context menu or pressing F12 while hovering on the identifier.
  
  

• Debugging: A debugging session can be initiated using the standard VS Code debug interface. This launches the VDMJ interpreter enabling commands to be issued through the terminal. For a list of the available commands type help.
  
  

• Proof Obligation Generation: Proof obligation generation can be performed for a specification by accessing the editor context menu (right-clicking in the editor window). Alternatively the explorer contex menu can be used by right-clicking a VDM file in the explorer window.
  
  

• Combinatiorial Testing: Combinatorial testing can be performed for a given specification by accessing the "Combinatorial Testing" menu in the activity bar.
  
  

• Translation to LaTeX and Word: A specification can be translated to LaTex or Word formats by accessing the editor context menu by right-clicking in the editor.
  
  

• Java code generation: From a specification you can generate Java code by accessing the editor context menu by right-clicking in the editor.

• Dependency graph generation: A dependency graph of the specification can be generated by accessing the editor context menu by right-clicking in the editor. This will generate a graphviz file (.dot) which can be displayed graphically elsewhere, e.g. by installing a graphviz extension such as vscode-graphviz or graphviz-interactive-preview.

• Coverage report: An execution coverage report can be generated by accessing the editor context menu by right-clicking in the editor.

• Import of project examples: VDM-SL, VDM++, and VDM-RT project examples can be imported by accessing the explorer context menu by right-clicking in the explorer.

• Import of VDM libraries: VDM libraries can be added to a project by accessing the explorer context menu by right-clicking in the explorer.

Settings

This extension contributes the following settings:

• vdm-vscode.JVMArguments: Arguments for the JVM that is executing the server (e.g. -Xmx2g).
• vdm-vscode.annotationPaths: Comma separated list of folders and/or jar file paths for annotations that should be used with the language server.
• vdm-vscode.highPrecision: Use high precision server that use more memory for variables ("on" or "off").
• vdm-vscode.debug.activateServerLog: Log server actions ("on" or "off").
• vdm-vscode.debug.experimentalServer: Use an experimental/external server ("on" or "off"). If "on" the client will not launch a server but instead connect to one that is running in another process. E.g. executing the VDMJ server in a debugger.
• vdm-vscode.debug.lspPort: Port used for the LSP/SLSP connection when experimentalServer is "on".
• vdm-vscode.debug.dapPort: Port used for the DAP connection when experimentalServer is "on".
• vdm-vscode.stdio.activateStdoutLogging: Activate logging of stdout/stderr to terminal window.
• vdm-vscode.stdio.stdioLogPath: File path for directory that should be used to store stdout/stderr logs. If empty, terminal logging is used instead of file logging.

Publications

Jonas K. Rask, Frederik P. Madsen, Nick Battle, Hugo D. Macedo and Peter G. Larsen, Visual Studio Code VDM Support, The 18th Overture Workshop, December 2020 [PDF]

Jonas K. Rask, Frederik P. Madsen, Nick Battle, Hugo D. Macedo and Peter G. Larsen, The Specification Language Server Protocol: A Proposal for Standardised LSP Extensions, The 6th Workshop on Formal Integrated Development Environment, May 2021 [PDF]

Change Log

See change log here.

Issues

Submit an issue if you find a bug or have a suggestion for improving the extension.

Contributing

Contributions are very welcome. To do so either open an issue or feature request or fork the repo and submit a pull request. For further information see here.