boogie-friends

https://github.com/boogie-org/boogie-friends.git

git clone 'git://github.com/boogie-org/boogie-friends.git'
1

Boogie friends

A collection of tools for interacting with Boogie and related languages.

Emacs package (boogie-mode, dafny-mode)

The boogie-friends package is an experimental collection of Emacs modes for writing verified programs in languages of the Boogie family. Dafny and Boogie are the two currently supported languages. Features include:

In addition, the Dafny mode offers:

Some pictures:

A Dafny buffer

Dafny buffer in Emacs

Notice the error highlighting, the symbol beautification (forall appears as ), and the code folding on the last line!

A Boogie buffer

Boogie buffer in Emacs

Completion and snippets

Completion in Boogie Completion in Dafny Snippets

Documentation (Dafny only)

Dafny docs

Browsing the Boogie translation of a Dafny file

Dafny buffer in Emacs

Setup

Automatic

  1. Setup MELPA

    In your .emacs, add these three lines if you don't have them yet:

    (require 'package) ;; You might already have this line
    (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
    (package-initialize) ;; You might already have this line
  2. Install the package: M-x package-install RET boogie-friends RET

  3. Indicate the paths to your Dafny and Boogie installations:

    In your .emacs:

    (setq flycheck-dafny-executable "PATH-TO-DAFNY")
    (setq flycheck-boogie-executable "PATH-TO-BOOGIE")
    (setq boogie-friends-profile-analyzer-executable "PATH-TO-Z3-AXIOM-PROFILER") ;; Optional

Keybindings

All modes

Dafny and Boogie

Dafny only

Tips

General

Real-time error highlighting

Real-time error highlighting is enabled by default for all languages. You can disable it:

Font support

If you see blocks instead of proper characters, or tall characters, or ugly characters:

  1. Install a good font and restart Emacs (Arial Unicode, Cambria, Segoe UI Symbol, DejaVu Sans Mono, FreeMono, STIX, Unifont and Symbola should all work).

  2. If that doesn't fix it, setup font fallback by adding the following to your .emacs (replace "Symbola" by the name of your font): elisp (set-fontset-font t 'unicode (font-spec :name "Symbola") nil 'append)

  3. If that still doesn't work, turn of prettification entirely by adding the following to setup-boogie-friends above: elisp (prettify-symbols-mode -1)

If you don't like the way one particular symbol is rendered, you can adjust the font for just that one:

(set-fontset-font t (cons ?≔ ?≔) "FreeSerif" nil 'prepend)

Profiling

A typical profiling workflow proceeds as follows:

  1. Open a file for which verification is slow, or times out.
  2. Use C-c C-t to generate a trace (the default timeout is set to 30s; you can customize it by changing boogie-friends-profiler-timeout).
  3. Use C-c C-p to profile a function. The slowest method (as determined by the trace) is presented first.
  4. Marvel at the intricacies of the axiom profiler.

Note: The axiom profiler works best if it has a Boogie source file to look at; thus, when profiling a Dafny source file, boogie-friends transparently saves it as a translated Boogie file first, and then runs Boogie (with profiling enabled) on it. Thus the profiler is Boogie in all cases, and custom prover arguments need to be set for Boogie if they are to be taken into account for profiling (for tracing and translation, however, Dafny's settings apply).

Custom prover configurations

Each time boogie-friends calls a prover, it collects arguments from four sources:

LANGUAGE-prover-local-args, another list of extra flags. This is empty by default, and is a good place to add per-file or per-directory flags (see below).

An example configuration might thus look like this:

;; Don't allow assumptions
(setq dafny-prover-custom-args '("/noCheating:1"))

;; Get more debug output when verifying with C-u C-c C-c
(setq dafny-prover-alternate-args '("/proverWarnings:2" "/traceverify" "/z3opt:TRACE=true" "/trace" "/traceTimes" "/tracePOs"))

The LANGUAGE-prover-local-args is useful if a file requires specific flags (maybe /vcsMaxKeepGoingSplits, for example): in that case you can set the LANGUAGE-prover-local-args in just that file or in the corresponding directory.

For example, you can add the following to the top of a file:

// -*- dafny-prover-local-args: ("/vcsMaxKeepGoingSplits:5" "/proverMemoryLimit:250") -*-

Acknowledgments

The documentation that ships with this package is auto-generated from the Dafny Quick Reference.

Pull requests are welcome!

Clone the repo:

mkdir -p ~/.emacs.d/lisp/ && cd ~/.emacs.d/lisp/
git clone https://github.com/boogie-org/boogie-friends

Then in your .emacs (in addition to the stuff above):

(add-to-list 'load-path "~/.emacs.d/lisp/boogie-friends/emacs/")
(require 'dafny-mode)
(require 'boogie-mode)