-
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) |
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
.
Description missing
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