Emacs packages for writing and analysing VDM specifications using VDM-SL, VDM++ and VDM-RT.
vdm-mode currently supports the following features:
- Syntax highlighting and editing
- Replacement of ASCII syntax (e.g.
lambda) with more aesthetically looking symbols (e.g.
- On the fly syntax checking using Flycheck
- VDM YASnippets
- REPL (read–eval–print loop) support based on
- Integration with VDMJ and Overture
Installation and configuration
The features described above are packaged separately as
vdm-comint. The last three
packages are optional but necessary to use the VDM snippets, enable
syntax checking and using the REPL, respectively.
Installation using MELPA (recommended)
available via MELPA and can be installed by executing the following
package-install RET vdm-mode RET package-install RET flycheck-vdm RET package-install RET vdm-snippets RET package-install RET vdm-comint RET
For manual installation, download the files from this repository and
add them to your
(add-to-list 'load-path "/folder/where/vdm-mode/is/")
Add the following to your Emacs configuration:
(require 'vdm-mode) (setq flycheck-vdm-tool-jar-path "/path/to/vdm-tool-jar") (vdm-mode-setup) (require 'vdm-comint)
The VDM interpreter used by
vdm-comint can be set either using
flycheck-vdm-tool-jar-path (as shown in the configuration above) or
vdm-comint-command (for example, if you do not wish to use
flycheck-vdm). By default
vdm-comint-command is preferred over
flycheck-vdm-tool-jar-path when the former is set (i.e. not nil).
By default the smartparens package treats
` as a pair, which is
vdm-comint-mode. If you are using
this package and want to prevent this behaviour then add the following
to your configuration:
;; Inconvenient to treat ` as a pair in vdm-mode and vdm-comint-mode (eval-after-load 'smartparens '(sp-local-pair #'vdm-mode "`" nil :actions nil)) (eval-after-load 'smartparens '(sp-local-pair #'vdm-comint-mode "`" nil :actions nil))
Recognised file extensions
The following file extensions are recognised as VDM files:
To enable syntax checking of VDM files
must contain a path to either a VDMJ or Overture jar file. The syntax
checker integration has been developed using Flycheck.
vdm-mode offers several VDM YASnippets to improve the editing
yas-insert-snippet is a useful way to obtain an
overview of the different snippets currently offered by
vdm-mode only performs syntax checking of the current
buffer. However, for large models,
vdm-mode uses a special file
.vdm-project to group files into VDM projects or multi-file
models. As an example, consider the VDM project structure below, which
lists three VDM files.
project-root-folder | +-- .vdm-project +-- A.vdmsl +-- B.vdmsl +-- sub-folder +-- C.vdmsl
Every time syntax checking is triggered
vdm-mode locates the root of
the project (if it exists) and recursively finds all VDM files
associated with that project. These files are then passed as
arguments to the underlying VDM tool, which performs the syntax
check. A VDM project may be created using the
vdm-comint currently exposes the following functions:
vdm-comint-load-project-or-switch-to-replSwitch to existing REPL or load the current VDM project in a new REPL.
vdm-comint-start-or-switch-to-replSwitch to existing REPL or start a new one (without loading any VDM files).
vdm-comint-send-regionSend the current region to the REPL. If no region is selected, you can manually input an expression.
vdm-comint-kill-repl Kill repl, if it exists.
If you have any ideas for how to improve
vdm-mode feel free to
create an issue or submit a pull request.