Dafny
![]() | |
Paradigm | Imperative, functional |
---|---|
Designed by | K. Rustan M. Leino |
Developer | Microsoft Research |
First appeared | 2009 |
Stable release | 3.0.0
/ February 3, 2021 |
Typing discipline | Static, strong, safe |
License | MIT License |
Filename extensions | .dfy |
Website | research |
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[1] for reasoning about side effects.[2] Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is widely used in teaching and 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 to provide a simple introduction to formal specification and verification and has been used widely in teaching. Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations.[7][8]
Data types[]
![]() | This section does not cite any sources. (January 2018) |
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.
Imperative features[]
![]() | This section does not cite any sources. (January 2018) |
Dafny supports proofs of imperative programs based on the ideas of Hoare logic. The following illustrates many such 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 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 prior to 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 provides illustrates:
method sumAndZero(ns:array<int>) returns (sum:nat)
requires ns != null
requires forall i :: 0 <= i < ns.Length ==> ns[i] >= 0
modifies ns
{
var i:int := 0;
var arr:array<int> := ns; // because parameters cannot be assigned
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 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: remove the redundant assignment arr[i] := arr[i];
; or, add the loop invariant invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0
Dafny additionally employs limited static analysis to infer simple loop invariants where possible. In the example above, it would seem the loop invariant invariant i >= 0
is also required as variable i
is mutated within the loop. Whilst the underlying logic does require such an invariant, Dafny automatically infers this and, hence, it can be omitted at the source level.
Proof features[]
Dafny includes features which further support its use as a proof assistant. Whilst 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 is perhaps 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)
}
ghost method 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
in order 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[]
- Design by contract
References[]
- ^ Smans, Jan; Jacobs, Bart; Piessens, Frank (2009). Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic (PDF). Proceedings of the Conference on European Conference on Object Oriented Programming. pp. 148–172. doi:10.1007/978-3-642-03013-0_8.
- ^ Leino, Rustan (2010). Dafny: An Automatic Program Verifier for Functional Correctness. Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. 348–370. doi:10.1007/978-3-642-17511-4_20.
- ^ Leino, Rustan; Monahan, Rosemary (2010). Dafny Meets the Verification Benchmarks Challenge (PDF). International Conference on Verified Software: Theories, Tools, and Experiments. pp. 112–116. doi:10.1007/978-3-642-15057-9_8.
- ^ Klebanov, Vladimir; et al. (2011). The 1st Verified Software Competition: Experience Report. Proceedings of the Conference on Formal Methods. pp. 154–168. CiteSeerX 10.1.1.221.6890. doi:10.1007/978-3-642-21437-0_14.
- ^ Bormer, Thorsten; et al. (2011). The COST IC0701 Verification Competition 2011. Proceedings of the Conference on Formal Verification of Object-Oriented Software. pp. 3–21. CiteSeerX 10.1.1.396.6170. doi:10.1007/978-3-642-31762-0_2.
- ^ Huisman, Marieke; Klebanov, Vladimir; Monahan, Rosemary (2015). "VerifyThis 2012: A Program Verification Competition" (PDF). Journal on Software Tools for Technology Transfer. 17 (6): 647–657. doi:10.1007/s10009-015-0396-8. S2CID 14301377.
- ^ "Z3 Homepage". 2019-02-07.
- ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Z3: An Efficient SMT Solver. Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis. pp. 337–340. doi:10.1007/978-3-540-78800-3_24.
Further reading[]
- Meyer, Bertrand; Nordio, Martin, eds. (2012). Tools for Practical Software Verification: International Summer School, LASER 2011, Elba Island, Italy, Revised Tutorial Lectures. Springer. ISBN 978-3642357459.
External links[]
- Academic programming languages
- Experimental programming languages
- Microsoft free software
- Microsoft programming languages
- Microsoft Research
- Programming languages created in 2009
- Proof assistants
- Software using the MIT license
- Statically typed programming languages