vdm-mode

Emacs packages for writing and analysing VDM specifications using VDM-SL, VDM++ and VDM-RT.

Editing:

REPL support:

Features

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. λ) using prettify-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

Installation and configuration

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.

Installation

Installation using MELPA (recommended)

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

Manual installation

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/")

Configuration

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))

Usage

Recognised file extensions

The following file extensions are recognised as VDM files:

• VDM-SL: .vdmsl and .vsl
• VDM++: .vdmpp and .vpp
• VDM-RT: .vdmrt and .vrt

Syntax checking

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 YASnippets

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.

Multi-file models

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.

REPL support

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.

Planned features

If you have any ideas for how to improve vdm-mode feel free to create an issue or submit a pull request.