Dafny 2 for Visual Studio Code (Legacy)

⚠ This plugin targets Dafny 2 and is deprecated. Consider switching to its successor that supports Dafny 3.0.0.

This extension adds Dafny support to Visual Studio Code.

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.

You can find more Examples below.

Shortcuts

Shortcut	Description
Ctrl+Shift+B or ⇧+⌘+B	Compile .dfy file to .dll or .exe, if there is a Main method
F5	Compile and run, if the source file has a Main method
F7	Show CounterExample
F8	Hide CounterExample

Tasks

Choose Tasks -> Run Task... to run one of the following:

Task	Description
Install DafnyServer	Downloads and installs the DafnyServer and sets the dafny.dafnyServerPath accordingly
Uninstall DafnyServer	Uninstalls the DafnyServer
Restart DafnyServer	Restarts the DafnyServer

Requirements

• The plugin needs a .NET runtime to run the DafnyServer. If you are not on Windows, please download a distribution from Mono.
  • Note: When you first open a Dafny file, the extension will prompt you to automatically install Dafny and Mono.
• In case you would like the plugin to use a different Dafny distribution, set the path to the DafnyServer.exe file via the dafny.dafnyServerPath user setting.

Extension Settings

Setting	Description	Default
dafny.basePath	Absolute path to the Dafny binary directory (which contains DafnyServer.exe).
dafny.monoExecutable	Mono executable with absolute path. Only necessary if mono is not in system PATH (you'll get an error if that's the case). Ignored on Windows when useMono is false.
dafny.useMono	Only applicable to Windows! Requires .NET 4.5 or higher when set to false.	false
dafny.automaticVerification	Verify as soon as the document is changed. When false, only verify on save.	true
dafny.automaticVerificationDelayMS	Delay in ms to wait after a document change before verifying document. This avoids syntax errors while typing. Only relevant if automaticVerification is true.	700
dafny.automaticShowCounterModel	Show CounterModel automatically if a proof fails. Might cause performance issues if true.	false
dafny.serverVerifyArguments	Additional arguments to pass to the "verify" command of the Dafny Server. E.g.["/timeLimit:40", "/vcsLoad:1"]	[]

Examples

Installation

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

Add null check

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

Compile and Run

Pressed F5 to compile and run the program.

Show Counter Example

Pressed F7 to show counter examples.

Contribute

This is a MIT licensed open-source project that lives from code contributions. All contributors are listed in our project readme.

We welcome your help! For a description of how you can contribute, as well as a list of issues you can work on, please visit the Dafny-VSCode GitHub repository.