-
Notifications
You must be signed in to change notification settings - Fork 6
Translation
You can translate the specification into different formats/languages, e.g. Latex and Word.
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.
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"
}
}
]
}
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
.
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.
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"]
}
],
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.
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.
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
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) |
- Home
- Getting Started
- Editor Features
- Including and Excluding Project Files
- Interpretation and Debugging
- Including Libraries
- Proof Obligation Generation
- Combinatorial Testing
- Animated Usage Examples
- Worked AlarmSL Examples
- Extension Settings
- Changing VDMJ Properties
- Translation
- Coverage
- Dependency Graph
- Real-time Log Viewer
- Code Generation
- Remote Control
- External File Formats
- Annotation Output
- Using VDM Values in Java
- VS Code Live Share
- Design
- The Specification Language Server Protocol
- For Developers/Contributors