Installing Dafny

The following instructions have been tested on Windows and Linux but should also work on Mac OS. If any problems occur, please contact the instructor.

Windows

For Visual Studio integration of Dafny, you need to build Boogie from sources. Currently, only Visual Studio 2010 is supported. You should be able to obtain a free academic license of Visual Studio via your CIMS account.

If you only want to use Dafny from the command line, simply follow the instructions below:

1. Download and unzip the Boogie distribution from the Boogie project web page. The Boogie distribution also includes Dafny.
2. Download and install the latest version of the Z3 Theorem Prover.
3. Create a Dafny test file and call it test.dfy.
4. Check whether Dafny is working by executing
   Dafny.exe /compile:0 test.dfy
   in your Boogie directory.

Linux and Mac OS

1. Download and unzip the Boogie distribution from the Boogie project web page. The Boogie distribution also includes Dafny.
2. Download the source code distribution of the Z3 Theorem Prover and build it.
3. Copy the Z3 executable to the Boggie directory and rename it z3.exe.
4. Install Mono. You will need version 2.8 or higher.
5. Create a Dafny test file and call it test.dfy.
6. Check whether Dafny is working by executing
   mono --runtime=v4.0.30319 Dafny.exe /compile:0 test.dfy
   in your Boogie directory.