projects

Dafny for Visual Studio Code

Visual Studio Code Plugin implementing Dafny Support

Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors.

The plugin is available on the Visual Studio Marketplace and on github.com/DafnyVSCode.

Features

  • Compile and run .dfy files.
    • Automatic installation of the newest Dafny version.
  • Automatic verification as one types.
    • Errors, warnings and hints are shown through the VSCode interface.
    • When there are no errors, you get a 👍 on the status bar.
  • Syntax highlighting thanks to sublime-dafny. See file LICENSE_sublime-dafny.rst for license.
  • Display counter example for failing proof.
  • IntelliSense for classes and CodeLens showing method references.

Examples

assertions animation

Installation

On the first start the plugin asks you to install Dafny automatically.

assertions animation

Add null check

Some diagnostics can be directly inserted with a quickfix at the beginning of a line.

assertions animation

Compile and Run

assertions animation

Show Counter Example

assertions animation