Try Dafny

The easiest way to get started with Dafny is to use rise4fun, where you can write and verify Dafny programs without having install anything. On rise4fun, you will also find the online Dafny tutorial.

Install the binaries

Windows: To install Dafny on your own machine, download Dafny.zip and save it to your disk. Then, before you open or unzip it, right-click on it and select Properties; at the bottom of the dialog, click the Unblock button and then the OK button. Now, open Dafny.zip and copy its contents into a directory on your machine. (You can now delete the Dafny.zip file.)

Then:

  • To run Dafny from the command line, simply run Dafny.exe from that directory.
  • To install Dafny for use inside Visual Studio 2012, double-click on DafnyLanguageService.vsix to run the installer. You may first need to uninstall the old version of the extension from within Visual Studio (Tools ==> Extensions and Updates). Then, whenever you open a file with the extension .dfy in Visual Studio, the Dafny mode will kick in. (If you don't intend to run Dafny from the command line, you can delete the directory into which you copied the contents of Dafny.zip.)
  • There is also a Dafny mode for Emacs.

Linux and Mac: Make sure you have Mono version 4. Then save the contents of the Dafny.zip for the appropriate version of your platform. You may need to make sure that `Dafny.exe` is marked as executable.  You can now run Dafny from the command line by invoking the script file `dafny`.  For an IDE, use the Dafny mode for Emacs.

Install the source code

First, install the following external dependencies:

Second, clone source code using TortoiseHg. The "clone source" can be found under "source code" tab "clone" of corresponding codeplex site:

Last, follow the conventions:

  • Visual Studio
    • Set "General:Tab" to "2 2"
    • For "C#:Formatting:NewLines" Turn everything off except the first option.
  • Change TortoiseHg "synchronize" button from default "none" to "Pos Pull: update".

 

Last edited Mar 29, 2016 at 6:44 PM by rustanleino, version 10

Comments

gumm Jul 30, 2015 at 11:57 AM 
Dafny on the webpage seems not to work correctly:
- the pre-installed examples work fine
- in most cases even a small change makes the program run for a while,
then quiet down without any feedback
I tried to download and install Z3 and Dafny as specified here.
A double-click on DafnyLanguageService.vsix yields an error message: "The extension manifest is invalid"
What now?

CraigStuntz Sep 14, 2014 at 3:38 AM 
You can avoid copying z3.exe to the Dafny folder by running Dafny as follows:

.\Dafny.exe /z3exe:'C:\Program Files\Z3\bin\z3.exe' ...

vineetp13 Jul 2, 2014 at 4:50 PM 
@nadia:
I just installed Dafny and ran it using VS 2012. I don't need to add Z3 to the direction where extension is installed.
However, I am curious why the Dafny.exe CLI executable does not generate a C# image while Visualstudio does.

nadia_polikarpova May 16, 2014 at 4:09 AM 
Note that the extension just crashes Visual Studio upon opening a Dafny file if it cannot find Z3. I had to copy Z3 into the directory where the extension is installed, which for me was C:\Users\<usename>\AppData\Local\Microsoft\VisualStudio\11.0\Extensions\hyua5ukc.o3s. It might be useful to add this to the description.

WaheedAhmad Oct 26, 2013 at 4:00 PM 
After installing the Dafny,I am getting an error "no input files has been specified". Any solution?

lawegyir Jun 6, 2013 at 2:53 PM 
when i install the tool i got the error that no input files has been specified! any solution??

balzers Feb 2, 2013 at 2:22 PM 
It would be helpful to point out how to disable an already installed Dafny language extension in Visual Studio. I did it through the menu Tools/Extensions and Updates.