/gobra-mode

Support for gobra verification tool

Primary LanguageEmacs Lisp

Gobra-mode for Emacs

Adds support to the Emacs IDE for Gobra.

Installation

This package is under heavy development. Thus, it is not published in any package archives.

To install it, one must clone the repository:

git clone git@github.com:Dspil/gobra-mode.git

Then, add the following lines in your init.el.

(add-to-list 'load-path "<gobra-mode repo path>")
(use-package gobra-mode)
(setq gobra-jar-path "<gobra jar file path>")
(setq gobra-z3-path "<Z3 executable path>")

Usage

Default keybindings:

  • C-c C-v: Verifies the file corresponding to the current buffer.
  • C-c C-g: Goifies the current buffer.
  • C-c C-c: Opens the generated Viper code in a new buffer.
  • C-c C-a: Spawns a construction buffer through which the arguments passed to gobra are manipulated.