#+STARTUP: showall

#+TITLE: vdm-mode


[[https://melpa.org/#/vdm-mode][file:https://melpa.org/packages/vdm-mode-badge.svg]]
[[http://melpa-stable.milkbox.net/#/vdm-mode][file:https://stable.melpa.org/packages/vdm-mode-badge.svg]]
[[http://www.gnu.org/licenses/gpl-3.0.html][https://img.shields.io/:license-gpl3-blue.svg?style=flat-square]]


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

Editing:

[[file:gifs/editing-demo.gif]]

REPL support:

[[file:gifs/repl-demo.gif]]

* 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 [[https://github.com/flycheck/flycheck][Flycheck]]  
- VDM [[https://github.com/joaotavora/yasnippet][YASnippets]]
- REPL (read–eval–print loop) support based on ~comint~
- Integration with [[https://github.com/nickbattle/vdmj][VDMJ]] and [[https://github.com/overturetool/overture][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 [[https://melpa.org][MELPA]] and can be installed by executing the following
commands:

#+BEGIN_SRC elisp
package-install RET vdm-mode RET
package-install RET flycheck-vdm RET
package-install RET vdm-snippets RET
package-install RET vdm-comint RET
#+END_SRC

*** Manual installation

For manual installation, download the files from this repository and
add them to your ~load-path~:

#+BEGIN_SRC elisp
(add-to-list 'load-path "/folder/where/vdm-mode/is/")
#+END_SRC

** Configuration

Add the following to your Emacs configuration:

#+BEGIN_SRC elisp
(require 'vdm-mode)
(setq flycheck-vdm-tool-jar-path "/path/to/vdm-tool-jar")
(vdm-mode-setup)

(require 'vdm-comint)
#+END_SRC

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 [[https://github.com/Fuco1/smartparens][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:

#+BEGIN_SRC elisp
;; 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))
#+END_SRC

* 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 [[https://github.com/nickbattle/vdmj][VDMJ]] or [[https://github.com/overturetool/overture][Overture]] jar file. The syntax
checker integration has been developed using [[https://github.com/flycheck/flycheck][Flycheck]].

** VDM YASnippets

~vdm-mode~ offers several VDM [[https://github.com/joaotavora/yasnippet][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.

#+begin_src ditaa
  project-root-folder   
  |
  +-- .vdm-project
  +-- A.vdmsl
  +-- B.vdmsl
  +-- sub-folder
      +-- C.vdmsl
#+end_src

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.