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.
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
In Visual Studio Code just type @id:overturetool.vdm-vscode in the Extensions view Search box or type vdm and select VDM VSCode.
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.
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.
This extension contributes a number of settings. Click here for a detailed overview.
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]
N. Battle and P. G. Larsen, Towards Operation Proof Obligation Generation in VDM, In Proceesings of the 23rd Overture Workshop, 2025 [PDF]
N.Battle and M.Ellyton, QuickCheck for VDM, In Proceedings of the 22nd Overture Workshop, 2024 [PDF]
See change log here.
Submit an issue if you find a bug or have a suggestion for improving the extension.
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.
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 and Outline integration
- Debugging (including function breakpoints and improved execution)
- Proof Obligation Generation (POG)
- Integrated QuickCheck support in the POG view
- Interactive Proof Obligations (hover info, inline feedback, code lenses)
- Combinatorial Testing
- Translation to LaTeX and Word
- Java code generation
- Dependency graph generation
- Coverage report
- Import of project examples
- Import of VDM libraries
- Snippets
- Quick Interpreter for evaluating standalone expressions
- Class hierarchy visualisation (VDM++/RT)
- Further improvements to syntax highlighting
- Additional debugging enhancements
- Improved workspace handling in the Combinatorial Testing view
- Continued usability and stability improvements