ws13 fmsoft dafny-installation

Dafny is an imperative, object-oriented programming language with classes and inductive datatypes, and specification constructs for describing intended behavior. The Dafny verifier checks that programs live up to their specifications. To do this, it ultimately relies on the Z3 SMT solver.

Being “academic tools” they require some effort to get them installed, but that is just part of the fun (?!) of using them; so here we go…

1. The first thing is to get a working version of Z3. There are pre-compiled binaries available for Windows, OSX, FreeBSD, Ubuntu and Debian available here. Otherwise, we have to compile from sources:

     $ git clone https://git01.codeplex.com/z3  # gets the sources
     $ cd z3
     $ autoconf
     $ ./configure
     $ python scripts/mk_make.py
     $ cd build
     $ make
     $ ./z3   # we run it to verify it built ok...
   

2. Second, to run Dafny, non-Windows users need a working installation of the mono runtime. If running mono on a terminal issues an error, one needs to install the package. Linux users can get it using their package manager (e.g. sudo apt-get install mono-complete on Ubuntu). OS X users can download the Mono.framework from here (select MRE, not SDK).
3. Finally, we install the Dafny verifying-compiler:
   1. Download Dafny.zip from here.
   2. Unzip the downloaded file to, say, ~/tools/Dafny.
   3. Copy the binary of z3 to ~/tools/Dafny, call it z3.exe (the .exe is crucial). For example, you can use a command such as cp ~/tools/z3/buld/z3 ~/tools/Dafny/z3.exe. NB. This may not be necessary in case z3 was installed and is on the path.
   4. Finally, time to check if all this effort was worth it. Download this example Dafny file and try to verify it running

        $ mono Dafny.exe mul.dfy