Dafny

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, using the modifies clause. Dafny also provides a range of immutable collection types including: sequences (e.g. seq<int>), sets (e.g. set<int>), maps (map<int,int>), tuples, inductive datatypes and mutable arrays (e.g. array<int>). ==Imperative features==

The following illustrates many of the features in Dafny, including the use of preconditions, postconditions, loop invariants and loop variants. method max(arr:array) returns (max:int) // Array must have at least one element requires arr.Length > 0 // Return cannot be smaller than any element in array ensures forall j : int :: j >= 0 && j max >= arr[j] // Return must match some element in array ensures exists j : int :: j>=0 && j = 0 && j max >= arr[j] // Some element seen so far matches max invariant exists j:int :: j >= 0 && j max) { max := arr[i]; } // Continue through array i := i + 1; } } This example 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). ==Loop invariants==

The treatment of loop invariants in Dafny differs from traditional Hoare logic. Variables mutated in a loop are treated such that (most) information known about them before the loop is discarded. Information required to prove properties of such variables must be expressed explicitly in the loop invariant. In contrast, variables not mutated in the loop retain all information known about them beforehand. The following example illustrates using loops: method sumAndZero(arr: array) returns (sum: nat) requires forall i :: 0 arr[i] >= 0 modifies arr { var i: int := 0; sum := 0; // while(i This fails verification because Dafny cannot establish that (sum + arr[i]) >= 0 holds at the assignment. From the precondition, intuitively, forall i :: 0 arr[i] >= 0 holds in the loop since arr[i] := arr[i]; is a NOP. However, this assignment causes Dafny to treat arr as a mutable variable and drop information known about it from before the loop. To verify this program in Dafny we can either (a) remove the redundant assignment arr[i] := arr[i];; or (b) add the loop invariant invariant forall i :: 0 arr[i] >= 0 Dafny also employs limited static program analysis to infer simple loop invariants where possible. In the example above, it would seem that the loop invariant invariant i >= 0 is also required as variable i is mutated within the loop. Whilst the underlying logic requires such an invariant, Dafny infers this automatically, and hence, it can be omitted at the source level. ==Proof features==

Dafny includes features which further support its use as a proof assistant. Although proofs of simple properties within a function or method (as shown above) are not unusual for tools of this nature, Dafny also allows the proof of properties between one function and another. As is common for a proof assistant, such proofs are often inductive in nature. Dafny may be unusual in employing method invocation as a mechanism for applying the inductive hypothesis. The following illustrates: datatype List = Nil | Link(data: int, next: List) function sum(l: List): int { match l case Nil => 0 case Link(d, n) => d + sum(n) } predicate isNatList(l: List) { match l case Nil => true case Link(d, n) => d >= 0 && isNatList(n) } lemma NatSumLemma(l: List, n: int) requires isNatList(l) && n == sum(l) ensures n >= 0 { match l case Nil => // Discharged Automatically case Link(data, next) => { // Apply Inductive Hypothesis NatSumLemma(next, sum(next)); // Check what known by Dafny assert data >= 0; } } Here, NatSumLemma proves a useful property between sum() and isNatList() (i.e. that isNatList(l) ==> (sum(l) >= 0)). The use of a ghost method for encoding lemmas and theorems is standard in Dafny with recursion employed for induction (typically, structural induction). Case analysis is performed using match statements and non-inductive cases are often discharged automatically. The verifier must also have complete access to the contents of a function or predicate to unroll them as necessary. This has implications when used in conjunction with access modifiers. Specifically, hiding the contents of a function using the protected modifier can limit what properties can be established about it. ==See also==