-
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"]
}
],
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