You can translate the specification into different formats/languages, e.g. Latex and Word.

Translate to Latex

To use this functionality, right-click on a file or folder and select VDM > Translate to LaTeX. This generates latex files corresponding to the VDM specification in the project subfolder named .generated/latex.

It is possible to use literate programming/specification with VS Code just as you can with Overture and VDMTools. To take advantage of this, you need to use the LaTeX text-processing system with plain VDM models mixed with textual documentation. The VDM model parts must be enclosed within \begin{vdm_al} and \end{vdm_al}. The text-parts outside these specification blocks are ignored by the VDM parser, though note that each source file must start with a recognizable LaTeX construct: a \documentclass, \section, \subsection or a LaTeX comment.

Settings

There are some options available for the translate to latex feature, that can be found at File > Preferences > Settings, they are:

Setting	Description	Default Value
Insert Coverage Tables	If enabled, inserts tables that summarise the coverage report in the latex translation files	Disabled (false)
Mark Coverage	If enabled, marks which parts of the specification have been covered and which have not been covered	Disabled (false)
Model Only	Only model part will be included in the Latex translation, i.e., everything enclosed within \begin{vdm_al} and \end{vdm_al}	Enabled (true)

Additionally the default appearance of LaTeX content in VDM documents is set to have the colour (hex) #7c7c7c and an italic font style. This can be changed by defining editor.tokenColorCustomizations in the settings.json file as follows substituting the values of 'fontStyle' and 'foreground':

"editor.tokenColorCustomizations": {
  "textMateRules": [
    {
      "scope": "meta.embedded.inline.latex", 
      "settings": {
          "fontStyle": "italic",
          "foreground": "#7c7c7c"
      }
    }
  ]
}

Translate to Word

To use this functionality, right-click on a file or folder and select VDM > Translate to Word. This generates word files corresponding to the VDM specification in the project subfolder named .generated/word.

Translate to Isabelle

To use this functionality, right-click on a file or folder and select VDM > Translate to Isabelle. This generates Isabelle *.thy files corresponding to the VDM specification in the project subfolder named .generated/isabelle. Note: The Translate to Isabelle feature is only available for VDM-SL.

The Isabelle translation plugin is currently being updated to allow it to be installed via a separate VSCode extension. If you need the functionality urgently, please contact the Overture team.

Translate to/from UML

Translate to UML

To use this functionality, right-click on a file or folder and select VDM > Translate to UML. This generates a PlantUML file with the extension .puml. PlantUML is a text based UML visualisation tool, which is used to represent your model using a UML class diagram.

To view the UML model, first make sure you have a PlantUML VS Code extension installed. If the recommended PlantUML extension is used, the diagram can be previewed using Alt + D. Similarly, the diagram can be exported by bringing up the command palette and selecting PlantUML: Export Current Diagram and choosing the desired format.

Editing Diagram Parameters

The text at the top of the PlantUML file changes the look and export behaviour of the UML diagram. For exporting very large diagrams, skinparam dpi 300 can be added to increase the resolution of the image. For more information about changing the look of the diagram, refer to the skinparam section on the PlantUML website.

Translate from UML

To use this functionality, right-click on a PlantUML file and select Translate to VDM. Make sure that the file is not located in the .generated folder in your VS Code workspace, since this cancels the translation. To create a PlantUML VDM model, please refer to the PlantUML Class Diagram overview as well as the VDM-UML plugin documentation

Translate to/from FMI

Translate to FMI (Export as FMU)

In your VDM project folder, right-click on the explorer menu and select VDM > Overture FMU > Export Tool Wrapper FMU. This generates an FMU file in the '.generated.' folder.

Translate from FMI (Import modelDescription)

Right-click on the explorer menu and select VDM > Overture FMU > Import FMU Model description. This generates the corresponding VDM classes in the current folder. Caveat: If you run this in an empty folder the VDM extension may not be active. You can force it to be active by creating a .vdmpp/.vdmrt file in int.

General Settings

There are some options that apply generally across all translations that can be found at File > Preferences > Settings, they are:

Setting	Description	Default Value
Allow Single File Translation	If enabled, translate only the selected file. If disabled, translate is always applied to the whole project	Enabled (true)
Store All Translations	If enabled, stores each translation in a timestamped folder instead of overwriting the previous content	Disabled (false)