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]
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
- 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
- Improve syntax highlighting
- Improve debugging execution
- Show all workspace folders in the Combinatorial Testing view