Translation

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 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.

Getting the latest version

The VDM to Isabelle translation is provided by Leo Freitas and can be found here. Thus, it may not always be up to date with his latest development. If you want to make sure that you have the latest version, follow the guide in the README to compile the .jar file with the vdm2isa plugin.

You can then replace the existing .jar with the new one. Or link to the new jar using the setting vdm-vscode.server.plugins, like:

"vdm-vscode.server.plugins": [
    {
        "name" : "vdm2isa alpha release",
        "classname" : "plugins.ISAPluginSL",
        "jar" : "the/location/where/you/put/the/jar/vdm2isa-4.4.5-SNAPSHOT-220218.jar",
        "dialects": ["vdmsl"]
    }
],

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)