Emacs packages for writing and analysing VDM specifications using VDM-SL, VDM and VDM-RT.
Editing:
REPL support:
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.λ
) usingprettify-symbols-mode
- On the fly syntax checking using Flycheck
- VDM YASnippets
- REPL (read–eval–print loop) support based on
comint
- Integration with VDMJ and Overture
The features described above are packaged separately as vdm-mode
,
vdm-snippets
, flycheck-vdm
and vdm-comint
. The last three
packages are optional but necessary to use the VDM snippets, enable
syntax checking and using the REPL, respectively.
vdm-mode
, flycheck-vdm
, vdm-snippets
and vdm-comint
are
available via MELPA and can be installed by executing the following
commands:
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 load-path
:
(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
using 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
inconvenient in vdm-mode
and 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))
The following file extensions are recognised as VDM files:
- VDM-SL:
.vdmsl
and.vsl
- VDM :
.vdmpp
and.vpp
- VDM-RT:
.vdmrt
and.vrt
To enable syntax checking of VDM files flycheck-vdm-tool-jar-path
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
experience. Calling yas-insert-snippet
is a useful way to obtain an
overview of the different snippets currently offered by vdm-mode
.
By default, vdm-mode
only performs syntax checking of the current
buffer. However, for large models, vdm-mode
uses a special file
named .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-mode-create-project
function.
vdm-comint
currently exposes the following functions:
vdm-comint-load-project-or-switch-to-repl
Switch to existing REPL or load the current VDM project in a new REPL.vdm-comint-start-or-switch-to-repl
Switch to existing REPL or start a new one (without loading any VDM files).vdm-comint-send-region
Send 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.