CS 477 - Formal Software Development Methods (Fall 2016)
Information on Dafny
DAFNY is a programming language that allows specifications and comes equipped with a program verifier. See the Dafny page for various resources, including quick references, tutorials, videos, etc.
You can use Dafny in different ways: you can try it online at Rise4Fun/Dafny or you can install it on your machine. We encourage you to install it on your machine for this course.
Go to
You can use Dafny in different ways: you can try it online at Rise4Fun/Dafny or you can install it on your machine. We encourage you to install it on your machine for this course.
Go to this page on the Dafny Github site and follow instructions to install the binary directly (Z3 will automtically get installe).
Executing Dafny
First install mono: Then install Dafny: Executing Dafny Windows machines
./Dafny.exe /compile:0 filename.dfy
Linux or Mac machines
Follow the instructions below to install the command line version of Dafny. These instructions have been tested for macOS 10.12 (should also work for 10.11), and Linux (Ubuntu 14.04).
Installation Guides for macOS, Linux and Windows are provided in the following website: http://www.mono-project.com/docs/getting-started/install/.
Download and unzip the latest release of Dafny corresponding to your OS from the Dafny project website:
https://github.com/Microsoft/dafny/releases/tag/v1.9.8
mono Dafny.exe /compile:0 filename.dfy