Installing Dafny

Follow the instructions below to install the command line version of Dafny. These instructions have been tested for Mac OS, but should also work for Linux and Windows.

Windows

1. Download and unzip Dafny from the Dafny project webpage.
2. Download latest version of the Z3 Theorem Prover.
3. Create a Dafny test file and call it test.dfy.
4. While in the Dafny directory, check whether Dafny is working by executing:
   Dafny.exe /compile:0 test.dfy
   or
   Dafny.exe test.dfy

Linux and Mac OS

1. Download and unzip Dafny from the Dafny project webpage.
2. Download latest version of the Z3 Theorem Prover. Build it following the instructions in the README file.
3. Copy the Z3 executable to the Dafny 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. While in the Dafny directory, check whether Dafny is working by executing:
   mono Dafny.exe /compile:0 test.dfy
   or
   mono Dafny.exe test.dfy