Homepage: https://github.com/boogie-org/boogie-friends
Author: Clément Pit-Claudel
Updated:
A collection of programming modes for Boogie, Dafny, and Z3 (SMTLIB v2)
This package is a collection of tools for writing verified programs in languages of the Boogie family. Dafny and Boogie are the two currently supported languages. Features include: * Syntax highlighting * Real-time compilation (using flycheck) * Completion (using company) * Code folding (using hideshow) * Prettification (using prettify-symbols-mode) In addition, the Dafny mode offers: * (A few) Snippets (using yasnippet) * (Some) In-Emacs documentation (using shr) * (Experimental) Navigation between Dafny and Boogie source files * (Some support for) indentation * (Some support for) jumping to a definition * (Experimental) Support for using Dafny as a verification server See https://github.com/boogie-org/boogie-friends/ for a full description. The documentation that accompanies certain snippets in dafny-mode was not written as part of this package; it is automatically generated from Dafny's quick reference guide.