Dafny

Dafny

Paradigm	Imperative, Functional
Designed by	K. Rustan M. Leino
First appeared	2009
Stable release	2.0.0 / September 23, 2017 (2017-09-23)
Typing discipline	Static, strong, safe
License	MIT
Website	research.microsoft.com/dafny

Dafny is an imperative compiled language that targets C# and supports formal specification through preconditions, postconditions, loop invariants and loop variants. The language combines ideas primarily from the Functional and Imperative paradigms, and includes limited support for Object-Oriented Programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is been used widely in teaching and features regularly in software verification competitions (e.g. VSTTE'08, VSCOMP'10, COST'11, and VerifyThis'12).

Dafny was designed to provide a simple introduction to formal specification and verification and has been used widely in teaching. Dafny follows in the lineage of many previous tools, including SPARK/Ada, ESC/Java, Spec#, Whiley, Why3 and Frama-C. Such tools rely on the use of automated theorem proving to discharge proof obligations unlike, for example, those based on dependent types (e.g. Idris, Agda) which require more human intervention. Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations.

Design

Dafny provides methods for implementation which may have side-effects and functions for use in specification which are pure. Methods consist of sequences of statements following a familiar imperative style whilst, in contrast, the body of a function is simply an expression. Any side-effecting statements in a method (e.g. assigning an element of an array parameter) must be accounted for by noting which parameters can be mutated in the modifies clause. Dafny also provides a range of immutable collection types including: sequences (e.g. seq<int>), sets (e.g. set<int>) and maps (map<int,int>). In addition, mutable arrays (e.g. array<int>) are provided.

Example

The following example illustrates many of the interesting features in Dafny, including the use of preconditions, postconditions, loop invariants and loop variants.

method max(arr:array<int>) returns(max:int)
 // Array must have at least one element
 requires arr!=null && arr.Length > 0;
 // Return cannot be smaller than any element in array
 ensures (forall j :int :: (j >= 0 && j < arr.Length ==> max >= arr[j]));
 // Return must match some element in array
 ensures (exists j : int :: j>=0 && j < arr.Length && max==arr[j]);
{
  max:=arr[0];
  var i:int :=1;
  //
  while(i < arr.Length)
  // Indent at most arr.Length (needed to show i==arr.Length after loop)
  invariant (i<=arr.Length);
  // No element seen so far larger than max
  invariant (forall j:int :: j>=0 && j<i ==> max >= arr[j]);
  // Some element seen so far matches max
  invariant (exists j:int :: j>=0 && j<i && max == arr[j]);
  // Terminate when i == arr.Length
  decreases (arr.Length-i); 
  {
    // Update max if larger element encountered
    if(arr[i] > max){max := arr[i];}
    // Continue through array
    i := i + 1;
  }
}

This examples computes the maximum element of an array. The method's precondition and postcondition are given with the requires and ensures clauses (respectively). Likewise, the loop invariant and loop variant are given through the invariant and decreases clauses (respectively).