Getting Started

System Requirements

In order to install and use Visual Studio Code and the VDM VSCode extension, you must have the following:

• An operating system that supports Visual Studio Code (Windows 8, 10, 11; various Linux systems; MacOS 10.11+)
• Visual Studio Code ≥ v. 1.49.0 (To use the latest version of the extension you will usually need the latest version of Visual Studio Code too)
• Java ≥ v. 11 (You MUST have Java installed on your system. Without Java, the VDM extension will install but it will not function at all. If Java is missing or outdated, the extension will display an error message).

Installation

Installing VDM VSCode is simple. You can find it in Visual Studio Code Marketplace, or type "@id:overturetool.vdm-vscode" or "vdm-vscode" in the Extensions view search box. See the official marketplace documentation for more details.

Creating New Projects and Workspaces

After installation, you can start creating new projects and organising them into workspaces of related projects. You can also import projects from a large number of examples distributed with the VDM VSCode extension.

Details of how to do this are available on the Projects and Workspaces page.

Developing VDM Specifications

VDM VSCode offers a complete set of features to enable you to develop and test VDM specifications. Features include:

• Editor Features
  • Syntax Highlighting
  • Syntax and Type Checking
  • Snippets
  • Smart Navigation
  • Outline Navigation
  • Code Completion
• Interpretation and Debugging
  • Starting the Interpreter
  • Configuring Launches
  • Launch and Debug Lenses
  • Advanced Launch Configurations
• Including Libraries
  • Standard Libraries
  • Including Custom Libraries
  • Encoding
• Proof Obligation Generation
  • The Proof Obligation View
  • Categories
• Combinatorial Testing
• Animated Usage Examples
• Extension Settings
• Changing VDMJ Properties
• Translation
  • Translate to Latex
  • Translate to Word
  • Translate to Isabelle
  • Settings
• Coverage
  • Generation
  • Visualization
• Dependency Graph
  • Generating Dependency Graph
  • Visualising the Dependency Graph
• Real-time Log Viewer
  • Opening the Log Viewer
  • Utilising the Log Viewer
  • Settings
  • Known Issues
• Code Generation
  • Java Code Generation

See these animated usage examples for an overview of how to use some features of the extension. Or see the respective pages for each of the features.