| Dafny | |
|---|---|
 | |
| Paradigm | Imperative,functional |
| Designed by | K. Rustan M. Leino |
| Developer | Microsoft Research |
| First appeared | 2009; 17 years ago (2009) |
| Stable release | 4.11.0 / August 25, 2025; 5 months ago (2025-08-25) |
| Typing discipline | Static,strong, safe |
| License | MIT |
| Filename extensions | .dfy |
| Website | dafny |
Dafny is animperative andfunctionalcompiled language that compiles to otherprogramming languages, such asC#,Java,JavaScript,Go, andPython. It supportsformal specification throughpreconditions,postconditions,loop invariants,loop variants, termination specifications and read/write framing specifications. The language combines ideas from thefunctional programming andimperative programming paradigms; it includes support forobject-oriented programming. Features includegeneric classes,dynamic allocation,inductive datatypes and a variation ofseparation logic known asimplicit dynamic frames[1] for reasoning about side effects.[2] Dafny was created by Rustan Leino atMicrosoft Research after his prior work on developing ESC/Modula-3,ESC/Java, and Spec#.
Dafny is regularly featured in software verification competitions (e.g. VSTTE'08,[3] VSCOMP'10,[4] COST'11,[5] and VerifyThis'12[6]).
Dafny was designed as a verification-aware programming language, requiring verification along with code development. It thus fits theCorrect by Construction software development paradigm. Verification proofs are supported by a mathematical toolbox that includes mathematical integers and reals, bit-vectors, sequences, sets, multisets, infinite sequences and sets, induction, co-induction, and calculational proofs. Verification obligations are discharged automatically, given sufficient specification. Dafny uses some program analysis to infer many specification assertions, reducing the burden on the user of writing specifications. The general proof framework is that ofHoare logic.
Dafny builds on the Boogieintermediate language which uses theZ3 automated theorem prover for discharging proof obligations.[7][8]
 | This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(January 2018) (Learn how and when to remove this message) |
Dafny provides methods for implementation which may haveside-effects and functions for use in specification which arepure.[9] 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 themodifies clause. Dafny also provides a range ofimmutable collection types including: sequences (e.g.seq<int>), sets (e.g.set<int>), maps (map<int,int>), tuples, inductive datatypes andmutable arrays (e.g.array<int>).
| This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(January 2018) (Learn how and when to remove this message) |
The following illustrates many of the features in Dafny, including the use of preconditions, postconditions, loop invariants and loop variants.
methodmax(arr:array<int>)returns(max:int)// Array must have at least one elementrequiresarr.Length>0// Return cannot be smaller than any element in arrayensuresforallj:int::j>=0&&j<arr.Length==>max>=arr[j]// Return must match some element in arrayensuresexistsj:int::j>=0&&j<arr.Length&&max==arr[j]{max:=arr[0];vari:int:=1;//while(i<arr.Length)// Index at most arr.Length (needed to show i==arr.Length after loop)invarianti<=arr.Length// No element seen so far larger than maxinvariantforallj:int::j>=0&&j<i==>max>=arr[j]// Some element seen so far matches maxinvariantexistsj:int::j>=0&&j<i&&max==arr[j]// arr.Length - i decreases at every step and is lower-bounded by 0decreasesarr.Length-i{// Update max if larger element encounteredif(arr[i]>max){max:=arr[i];}// Continue through arrayi:=i+1;}}
This example computes the maximum element of an array. The method's precondition and postcondition are given with therequires andensures clauses (respectively). Likewise, the loop invariant and loop variant are given through theinvariant anddecreases clauses (respectively).
The treatment of loop invariants in Dafny differs from traditionalHoare 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:
methodsumAndZero(arr:array<int>)returns(sum:nat)requiresforalli::0<=i<arr.Length==>arr[i]>=0modifiesarr{vari:int:=0;sum:=0;//while(i<arr.Length){sum:=sum+arr[i];arr[i]:=arr[i];i:=i+1;}}
This fails verification because Dafny cannot establish that(sum + arr[i]) >= 0 holds at the assignment. From the precondition, intuitively,forall i :: 0 <= i < arr.Length ==> arr[i] >= 0 holds in the loop sincearr[i] := arr[i]; is aNOP. However, this assignment causes Dafny to treatarr 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 assignmentarr[i] := arr[i];; or (b) add the loop invariantinvariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0
Dafny also employs limitedstatic program analysis to infer simple loop invariants where possible. In the example above, it would seem that the loop invariantinvariant i >= 0 is also required as variablei 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.
Dafny includes features which further support its use as aproof assistant. Although proofs of simple properties within afunction ormethod (as shown above) are not unusual for tools of this nature, Dafny also allows the proof of properties between onefunction and another. As is common for aproof assistant, such proofs are ofteninductive in nature. Dafny may be unusual in employing method invocation as a mechanism for applying the inductive hypothesis. The following illustrates:
datatypeList=Nil|Link(data:int,next:List)functionsum(l:List):int{matchlcaseNil=>0caseLink(d,n)=>d+sum(n)}predicateisNatList(l:List){matchlcaseNil=>truecaseLink(d,n)=>d>=0&&isNatList(n)}lemmaNatSumLemma(l:List,n:int)requiresisNatList(l)&&n==sum(l)ensuresn>=0{matchlcaseNil=>// Discharged AutomaticallycaseLink(data,next)=>{// Apply Inductive HypothesisNatSumLemma(next,sum(next));// Check what known by Dafnyassertdata>=0;}}
Here,NatSumLemma proves a useful propertybetweensum() andisNatList() (i.e. thatisNatList(l) ==> (sum(l) >= 0)). The use of aghost method for encodinglemmas and theorems is standard in Dafny with recursion employed for induction (typically,structural induction).Case analysis is performed usingmatch statements and non-inductive cases are often discharged automatically. The verifier must also have complete access to the contents of afunction orpredicate to unroll them as necessary. This has implications when used in conjunction withaccess modifiers. Specifically, hiding the contents of afunction using theprotected modifier can limit what properties can be established about it.
Microsoft development tools | |||||||
|---|---|---|---|---|---|---|---|
| Development environments |
| ||||||
| Languages | |||||||
| APIs and frameworks |
| ||||||
| Database |
| ||||||
| Source control | |||||||
| Testing and debugging | |||||||
| Delivery | |||||||
| Main projects |
| ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| MSR Labs applied research |
| ||||||||||||||
