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.

*If you are used to the Overture Tool IDE and would like to keep that syntax highlighting we suggest that you use the color theme Eclipse Classic Light or another eclipse color theme.

Wiki

Check out the wiki for the extension for information about how to get started, learning how to use the features, see developer notes and much more! Find the wiki at: https://github.com/overturetool/vdm-vscode/wiki

Installation

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

Requirements

Web extension

For now only the following limited feature set is available in the web version of the extension:

Syntax Highlighting
Snippets

Thus, most feature contributions relates to the desktop version of the extension.

Usage

Open a folder (single VDM project) or a workspace (multiple VDM projects) and then open a VDM file(.vdmsl, .vdmpp or .vdmrt) from the explorer window. This will automatically start the language server in the background.

Click here for an overview of how to use the features of the extension.

Settings

This extension contributes a number of settings. Click here for a detailed overview.

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]

Jonas K. Rask and Frederik P. Madsen, Decoupling of Core Analysis Support for Specification Languages from User Interfaces in Integrated Development Environments, Master's Thesis, Department of Engineering, Aarhus University, January 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.

Features

Following is a select number of features. For the full up to date list see the wiki.

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
Snippets

Future Work

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