This page contains some animated GIFs that demonstrate the usage of the tool. The aspects shown are covered elsewhere in the wiki too.

• Syntax Highlighting
• Syntax- and Type-checking
• Smart Navigation
• Debugging
  • Debugging Using Lenses
• Proof Obligation Generation
• Combinatiorial Testing
• Translation to LaTeX and Word
• Translation from and to UML
• Export to FMU
• Java Code Generation
• Dependency Graph Generation
• Coverage Report
• Import of Project Examples
• Import of VDM libraries
• Remote Control
• Snippets
• Real Time Log Viewer

VDM keywords are automatically highlighted.

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

Multiple actions exist 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.

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.

A debugging session can be initiated using the generated widgets next to executable VDM primitives.

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

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

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

A VDM++ or VDM-RT specification can be translated to the PlantUML format and a .puml file can be translated to VDM++ by accessing the editor context menu by right-clicking in the editor.

A VDM-RT specification can be exported as a tool wrapper FMU.

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

A dependency graph for 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.

An execution coverage report can be generated by accessing the editor context menu by right-clicking in the editor. The results from the latest coverage report or a user-defined coverage report (configurable in the settings) can be overlayed on the visible editors by a toggle in the focused editor title.

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

VDM libraries can be added to a project by accessing the context menu by right-clicking in the explorer or the editor. Libraries to choose from can be configured in the settings.

You can use the remote control option by adding a new configuration and selecting "VDM Debug: Remote Control (VDM-SL/++/RT).

You can press CTRL+space after typing the first few characters of a known VDM construct and Overture will offer its auto-completion. a proposal.

Opening a .rtlog file from a VDM-RT project will show a prompt asking if the log file should be viewed in the log viewer. The log viewer shows an architecture overview, an execution overview, a number of CPU overviews (one for each deployed CPU) and a diagram legend overview. The diagram in the execution overview and CPU overview(s) can be navigated in time by either choosing a start time or by the up and down arrows which will decrease or increase the current start time.