{"id":170169,"date":"2008-12-23T10:54:51","date_gmt":"2008-12-23T10:54:51","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/"},"modified":"2018-04-03T16:44:49","modified_gmt":"2018-04-03T23:44:49","slug":"dafny-a-language-and-program-verifier-for-functional-correctness","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/","title":{"rendered":"Dafny: A Language and Program Verifier for Functional Correctness"},"content":{"rendered":"<p class=\"asset-content\"><img loading=\"lazy\" decoding=\"async\" class=\"alignleft size-medium wp-image-214660\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/dafny-logo_sm-300x249.jpg\" alt=\"dafny-logo_sm\" width=\"300\" height=\"249\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/dafny-logo_sm-300x249.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/dafny-logo_sm.jpg 690w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/>Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs.<\/p>\n<p>The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and\u00a0inductive datatypes,\u00a0and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics.<\/p>\n<p>To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like sets and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code.<\/p>\n<p>The Dafny verifier is run as part of the compiler. As such, a programmer interacts with it much in the same way as with the static type checker\u2014when the tool produces errors, the programmer responds by changing the program\u2019s type declarations, specifications, and statements.<\/p>\n<p>The easiest way to try out <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/dafny\/Hello\">Dafny is in your web browser at rise4fun<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.\u00a0 Once you get a bit more serious, you may prefer to <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"https:\/\/github.com\/Microsoft\/dafny\" target=\"_self\">download<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> to run it on your machine.\u00a0 Although Dafny can be run from the command line (on Windows or other platforms), the preferred way to run it is in Microsoft Visual Studio 2010, where the Dafny verifier runs in the background while the programmer is editing the program.<\/p>\n<p>The Dafny verifier is powered by <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/boogie-an-intermediate-verification-language\/\">Boogie<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> and Z3.<\/p>\n<p>From verified programs, the Dafny compiler produces code (.dll or .exe) for the .NET platform.\u00a0 However, the facilities for interfacing with other .NET code are minimal.<\/p>\n<p>The <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"http:\/\/dafny.codeplex.com\/\" target=\"_self\">source code<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> for Dafny is available.<\/p>\n\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t<div\n\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\trole=\"group\"\n\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\tdata-target=\"#accordion-1\">\n\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t\t\t<ul class=\"accordion\" id=\"accordion-1\">\n\t\t\t\t\t\t\t\t<li class=\"m-0\">\n\t\t<h4 class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\ttype=\"button\"\n\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\tdata-target=\"#collapse-2\"\n\t\t\t\taria-expanded=\"false\"\n\t\t\t\taria-controls=\"collapse-2\"\n\t\t\t>\n\t\t\t\tLearn More\t\t\t<\/button>\n\t\t<\/h4>\n\t\t<div class=\"collapse\" id=\"collapse-2\">\n\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t<h2>Learn more<\/h2>\n<p>To become a user of Dafny, follow the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Dafny\/tutorial\/guide\">Dafny tutorial<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> online.<\/p>\n<p>You can also see Dafny in action in some episodes of <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/channel\/UCP2eLEql4tROYmIYm5mA27A\">Verification Corner<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n<p>To learn more about the features of Dafny, the Dafny Quick Reference may be for you.<\/p>\n<p>The following paper presents the salient features of Dafny, along with the Schorr-Waite algorithm written in Dafny.\u00a0 If\u00a0you&#8217;re scientifically or technically inclined, this is the one to read and cite:<\/p>\n<blockquote>\n<p>K. Rustan M. Leino.\u00a0 <strong>Dafny: An Automatic Program Verifier for Functional Correctness<\/strong>.\u00a0 In <em>LPAR-16<\/em>, volume 6355 of LNCS, pages 348-370.\u00a0 Springer, 2010. [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/dafny_krml203.pdf\">PDF<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>] [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/Dafny-LPAR-16.pptx\">slides from the conference presentation<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>]<\/p>\n<\/blockquote>\n<p dir=\"ltr\">To dig deeper into the technology behind Dafny, the following lecture notes from the Marktoberdorf 2008 summer school describe the encoding of Dafny into Boogie 2:<\/p>\n<blockquote>\n<p dir=\"ltr\">K. Rustan M. Leino.\u00a0 <strong>Specification and verification of object-oriented software<\/strong>.\u00a0 In <em>Engineering Methods and Tools for Software Safety and Security<\/em>, volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 231-266.\u00a0 IOS Press, 2009.\u00a0[<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/Dafny_krml190.pdf\">PDF<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>] [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/Leino-Lugano-2008-1.pptx\">slides from the lectures<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>]<\/p>\n<\/blockquote>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\">\n\t\t<h4 class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\ttype=\"button\"\n\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\tdata-target=\"#collapse-3\"\n\t\t\t\taria-expanded=\"false\"\n\t\t\t\taria-controls=\"collapse-3\"\n\t\t\t>\n\t\t\t\tQuick Reference\t\t\t<\/button>\n\t\t<\/h4>\n\t\t<div class=\"collapse\" id=\"collapse-3\">\n\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t<h1>Dafny Quick Reference<\/h1>\n<p>This page illustrates many of the most common language features in Dafny.\u00a0 In order to get you started more quickly, the descriptions here are simplified&#8211;this page is not\u00a0the language reference.\u00a0 For example, this pages does not go into modules, iterators, or refinement, which you won&#8217;t need until you write larger or more advanced programs in Dafny.<\/p>\n<h2>Programs<\/h2>\n<p>At the top level, a Dafny program (stored as a file with extension .dfy) is a set of declarations. The declarations introduce <em>types<\/em>,\u00a0<em>methods,<\/em> and <em>functions<\/em>, where the order of introduction is irrelevant.\u00a0 These user-defined\u00a0types include <em>classes<\/em> and <em>inductive datatypes<\/em>.\u00a0 The classes themselves also contain a set of declarations, introducing <em>fields<\/em>, methods, and functions.\u00a0 If the program contains a parameter-less method called Main, then execution of the compiled program starts there, but it is not necessary to have a main method to do verification.<\/p>\n<p>Comments start with \/\/ and go to the end of the line, or start with \/* and end with *\/ and can be nested.<\/p>\n<h2>Fields<\/h2>\n<p>In a class, a\u00a0field x of some type T is declared as:<\/p>\n<p>var x: T<\/p>\n<p>Unlike for local variables and bound variables, the type is required and will not be inferred. The field can be declared to be a ghost field by preceding the declaration with the keyword ghost. Dafny\u2019s types include bool for booleans, int for mathematical (that is, unbounded) integers, string for strings, user-defined classes and inductive datatypes, set<t> for a finite mathematical (immutable) set of T values (where T is a type), and seq<\/t><t> for a mathematical (immutable) sequence of T values. In addition, there are array types (which are like predefined \u201cclass\u201d types) of one and more dimensions, written array<\/t><t>, array2<\/t><t>, array3<\/t><t>, \u2026. The type object is a supertype of all class types, that is, an object denotes any reference, including null. Another useful type is nat, which denotes a subrange of int, namely the non-negative integers.<\/t><\/p>\n<h2>Methods<\/h2>\n<p>A method declaration (either at the top level or inside a class) has the form:<\/p>\n<p>method M(a: A, b: B, c: C) returns (x: X, y: Y, z: Y)requires Premodifies Frameensures Postdecreases Rank{Body}<\/p>\n<p>where a, b, c are the method\u2019s in-parameters, x, y, z are the method\u2019s out-parameters, Pre is a boolean expression denoting the method\u2019s precondition, Frame denotes a set of objects whose fields may be updated by the method, Post is a boolean expression denoting the method\u2019s postcondition, Rank is the method\u2019s variant function, and Body is a statement that implements the method. Frame can be a list of expressions, each of which is a set of objects or a single object, the latter standing for the singleton set consisting of that one object. The method\u2019s frame is the union of these sets, plus the set of objects allocated by the method body.\u00a0 For example, if c and d are parameters of a class type C, then<\/p>\n<p>modifies {c, d}<\/p>\n<p>modifies {c} + {d}<\/p>\n<p>modifies c, {d}<\/p>\n<p>modifies c, d<\/p>\n<p>all mean the same thing.<\/p>\n<p>If omitted, the pre- and postconditions default to true and the frame defaults to the empty set. The variant function is a list of expressions, denoting the unending lexicographic tuple consisting of the given expressions followed implicitly by \u201ctop\u201d elements. If omitted, Dafny will guess a variant function for the method, namely the lexicographic tuple that starts with the list of the method\u2019s in-parameters.<\/p>\n<p>A method can be declared as ghost by preceding the declaration with the keyword ghost. By default, a method in a class has an implicit receiver parameter, this. This parameter can be removed by preceding the method declaration with the keyword static. A static method M in a class C can be invoked by C.M(\u2026).<\/p>\n<p>In a class, a method can be declared to be a constructor method by replacing the keyword method with the keyword constructor. A constructor can only be called at the time an object is allocated (see object-creation examples below), and for a class that contains one or more constructors, object creation must be done in conjunction with a call to a constructor.\u00a0 Ordinarily, a method has a name, of course, but a class is allowed to have one constructor without a name&#8211;an <em>anonymous constructor<\/em>&#8211;like this:<\/p>\n<p>constructor (n: int)modifies this{Body}<\/p>\n<p>Often, ghost methods are used as lemmas.\u00a0 This can be made clearer in the program text by declaring the method with lemma instead of ghost method.<\/p>\n<p>Here is an example method that takes 3 integers as in-parameters and returns these in 3 out-parameters in sorted order:<\/p>\n<p>method Sort(a: int b: int, c: int) returns (x: int, y: int, z: int)ensures x <= y <= z && multiset{a, b, c} == multiset{x, y, z}{x, y, z := a, b, c;if z < y {y, z := z, y;}if y < x {x, y := y, x;}if z < y {y, z := z, y;}}<\/p>\n<h2>Functions<\/h2>\n<p>A function declaration (either at the top level or inside a class) has the form:<\/p>\n<p>function F(a: A, b: B, c: C): Trequires Prereads Frameensures Postdecreases Rank{Body}<\/p>\n<p>where a, b, c are the method\u2019s parameters, T is the type of the function\u2019s result, Pre is a boolean expression denoting the function\u2019s precondition, Frame denotes a set of objects whose fields the function body may depend on, Post is a boolean expression denoting the function\u2019s postcondition, Rank is the function\u2019s variant function, and Body is an expression that defines the function. The precondition allows a function to be partial, that is, the precondition says when the function is defined (and Dafny will verify that every use of the function meets the precondition). The postcondition is usually not needed, since the body of the function gives the full definition. However, the postcondition can be a convenient place to declare properties of the function that may require an inductive proof to establish. For example:<\/p>\n<p>function Factorial(n: int): intrequires 0 <= nensures 1 <= Factorial(n){if n == 0 then 1 else Factorial(n-1) * n}<\/p>\n<p>says that the result of Factorial is always positive, which Dafny verifies inductively from the function body. To refer to the function\u2019s result in the postcondition, use the function itself, as shown in the example.<\/p>\n<p>By default, a function is ghost, and cannot be called from non-ghost code. To make it non-ghost, replace the keyword function with the two keywords function method.\u00a0 A function that returns a boolean can be declared with the keyword predicate (and then eliding the colon and return type).<\/p>\n<p>By default, a function in a class has an implicit receiver parameter, this. This parameter can be removed by preceding the function declaration with the keyword static. A static function F in a class C can be invoked by F.M(\u2026). This can give a convenient way to declare a number of helper functions in a separate class.<\/p>\n<h2>Classes<\/h2>\n<p>A class is defined as follows:<\/p>\n<p>class C {\/\/ member declarations go here}<\/p>\n<p>where the members of the class (fields, methods, and functions) are defined (as described above) inside the curly braces.<\/p>\n<h2>Datatypes<\/h2>\n<p>An inductive datatype is a type whose values are created using a fixed set of constructors. A datatype Tree with constructors Leaf and Node is declared as follows:<\/p>\n<p>datatype Tree =\u00a0Leaf | Node(Tree, int, Tree)<\/p>\n<p>The constructors are separated by vertical bars. Parameter-less constructors need not use parentheses, as is shown here for Leaf.<\/p>\n<p>For each constructor Ct, the datatype implicitly declares a boolean member Ct?, which returns true for those values that have been constructed using Ct. For example, after the code snippet:<\/p>\n<p>var t0 := Leaf;var t1 := Node(t0, 5, t0);<\/p>\n<p>the expression t1.Node? evaluates to true and t0.Node? evaluates to false. Two datatype values are equal if they have been created using the same constructor and the same parameters to that constructor. Therefore, for parameter-less constructors like Leaf, t.Leaf? gives the same result as t == Leaf.<\/p>\n<p>A constructor can optionally declare a destructor for any of its parameters, which is done by introducing a name for the parameter. For example, if Tree were declared as:<\/p>\n<p>datatype Tree = Leaf | Node(left: Tree, data: int, right: Tree)<\/p>\n<p>then t1.data == 5 and t1.left == t0 hold after the code snippet above.<\/p>\n<h2>Generics<\/h2>\n<p>Dafny supports type parameters.\u00a0 That is, any class, inductive datatype, method, and function can have type parameters. These are declared in angle brackets after the name of what is being declared. For example:<\/p>\n<p>class MyMultiset<t> { \/*\u2026*\/ }datatype Tree<\/t><t> =\u00a0Leaf | Node(Tree<\/t><t>, T, Tree<\/t><t>)method Find<\/t><t>(key: T, collection: Tree<\/t><t>) { \/*\u2026*\/ }function IfThenElse<\/t><t>(b: bool, x: T, y: T): T { \/*\u2026*\/ }<\/t><\/p>\n<h2>Statements<\/h2>\n<p>Here are examples of the most common statements in Dafny.<\/p>\n<p>var LocalVariables := ExprList;Lvalues := ExprList;assert BoolExpr;print ExprList;<\/p>\n<p>if BoolExpr0 {Stmts0} else if BoolExpr1 {Stmts1} else {Stmts2}<\/p>\n<p>while BoolExprinvariant Invmodifies Framedecreases Rank{Stmts}<\/p>\n<p>match Expr {case Empty => Stmts0case Node(l, d, r) => Stmts1}<\/p>\n<p>break;return;<\/p>\n<p>The var statement introduces local variables (which are not allowed to shadow other variables declared inside the same set of most tightly enclosing curly braces). Each variable can optionally be followed by :T for any type T, which explicitly gives the preceding variable the type T (rather than being inferred). The ExprList with initial values is optional. To declare the variables as ghost variables, precede the declaration with the keyword ghost.<\/p>\n<p>The assignment statement assigns each right-hand side in ExprList to the corresponding left-hand side in Lvalues. These assignments are performed in parallel (more to the point, all necessary reads occur before the writes), so the left-hand sides must denote distinct L-values. Each right-hand side can be an expression or an object creation of one of the following forms:<\/p>\n<p>new Tnew T.Init(ExprList)new T(ExprList)new T[SizeExpr]new T[SizeExpr0, SizeExpr1]<\/p>\n<p>The first form allocates an object of type T. The second form additionally invokes an initialization method or constructor on the newly allocated object.\u00a0The third form shows\u00a0how the\u00a0syntax differs from the second form when the constructor called is anonymous.\u00a0 The other forms show examples of array allocations, in particular a one- and a two-dimensional array of T values, respectively.<\/p>\n<p>The entire right-hand side of an assignment can also be a method call, in which case the left-hand sides are the actual out-parameters (omitting the := if there are no out-parameters).<\/p>\n<p>The assert statement claims that the given expression evaluates to true (which is checked by the verifier).<\/p>\n<p>The print statement outputs to standard output the values of the given print expressions. Characters in strings can be escaped; for example, of interest for the print statement is that\u00a0n denotes a newline character inside a string.<\/p>\n<p>The if statement is the usual one. The example shows stringing together alternatives using else if. The else branch is optional, as usual.<\/p>\n<p>The while statement is the usual loop, where the invariant declaration gives a loop invariant, the modifies clause restricts the modification frame of the loop, and the decreases clause introduces a variant function for the loop. By default, the loop invariant is true, the modification frame is the same as in the enclosing context (usually the modifies clause of the enclosing method), and the variant function is guessed from the loop guard.<\/p>\n<p>The match statement evaluates the source Expr, an expression whose type is an inductive datatype, and then executes the case corresponding to which constructor was used to create the source datatype value, binding the constructor parameters to the given names.\u00a0 If they are not needed to mark the end of the\u00a0match statement, then the curly braces that surround the cases can be elided.<\/p>\n<p>The break statement can be used to exit loops, and the return statement can be used to exit a method.<\/p>\n<h2>Expressions<\/h2>\n<p>The expressions in Dafny are quite similar to those in Java-like languages. Here are some noteworthy differences.<\/p>\n<p>In addition to the short-circuiting boolean operators && (and) and || (or), Dafny has a short-circuiting implication operator ==> and an if-and-only-if operator <==>. As suggested by their widths, <==> has lower binding power than ==>, which in turn has lower binding power than && and ||.<\/p>\n<p>Dafny comparison expressions can be chaining, which means that comparisons \u201cin the same direction\u201d can be strung together. For example,<\/p>\n<p>0 <= i < j <= a.Length == N<\/p>\n<p>has the same meaning as:<\/p>\n<p>0 <= i && i < j && j <= a.Length && a.Length == N<\/p>\n<p>Note that boolean equality can be expressed using both == and <==>. There are two differences between these. First, == has a higher binding power than <==>. Second, == is <em>chaining<\/em> while <==> is <em>associative<\/em>. That is, a == b == c is the same as a == b && b == c, whereas a <==> b <==> c is the same as a <==> (b <==> c), which is also the same as (a <==> b) <==> c.<\/p>\n<p>Operations on integers are the usual ones, except that \/ (integer division) and % (integer modulo) follow the Euclidean definition, which means that % always results in a non-negative number. (Hence, when the first argument to \/ or % is negative, the result is different than what you get in C, Java, or C#, see <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/en.wikipedia.org\/wiki\/Modulo_operation\" target=\"_self\">http:\/\/en.wikipedia.org\/wiki\/Modulo_operation<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.)<\/p>\n<p>Dafny expressions include universal and existential quantifiers, which have the form:<\/p>\n<p>forall x :: Expr<\/p>\n<p>and likewise for exists, where x is a bound variable (which can be declared with an explicit type, as in x: T) and Expr is a boolean expression.<\/p>\n<p>Operations on sets include + (union), * (intersection), and &#8211; (set difference), as well as the set comparison operators < (proper subset), <= (subset), their duals > and >=, and !! (disjointness). The expression x in S says that x is a member of set S, and x !in S is a convenient way of writing !(x in S). To make a set from some elements, enclose them in curly braces. For example, {x,y} is the set consisting of x and y (which is a singleton set if x == y), {x} is the singleton set containing x, and {} is the empty set.<\/p>\n<p>Operations on sequences include + (concatenation) and the comparison operators < (proper prefix) and <= (prefix). Membership can be checked like for sets: x in S and x !in S. The length of a sequence S is denoted |S|, and the elements of such a sequence have indices from 0 to less than |S|. The expression S&#091;j&#093; denotes the element at index j of sequence S. The expression S&#091;m..n&#093;, where 0 <= m <= n <= |S|, returns a sequence whose elements are the n-m elements of S starting at index m (that is, from S&#091;m&#093;, S&#091;m+1&#093;, \u2026 up to but not including S&#091;n&#093;). The expression S&#091;m..&#093; (often called \u201cdrop m\u201d) is the same as S&#091;m..|S|&#093;, that is, it returns the sequence whose elements are all but the first m elements of S. The expression S&#091;..n&#093; (often called \u201ctake n\u201d) is the same as S&#091;0..n&#093;, that is, it returns the sequence that consists of the first n elements of S. If j is a valid index into sequence S, then the expression S&#091;j := x&#093; is the sequence that is like S except that it has x at index j. Finally, to make a sequence from some elements, enclose them in square brackets. For example, &#091;x,y&#093; is the sequence consisting of the two elements x and y such that &#091;x,y&#093;&#091;0&#093; == x and &#091;x,y&#093;&#091;1&#093; == y, &#091;x&#093; is the singleton sequence whose only element is x, and &#091;&#093; is the empty sequence.<\/p>\n<p>The if-then-else expression has the form:<\/p>\n<p>if BoolExpr then Expr0 else Else1<\/p>\n<p>where Expr0 and Expr1 are any expressions of the same type. Unlike the if statement, the if-then-else expression uses the then\u00a0keyword, and must include an explicit else branch.<\/p>\n<p>The match expression is analogous to the\u00a0match statement and has the form:<\/p>\n<p>match Expr {case Empty => Expr0case Node(l, d, r) => Expr1}<\/p>\n<p>The curly braces can be used to mark the end of the match expression, but most commonly this is not needed and the curly braces can then be elided.<\/p>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\">\n\t\t<h4 class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\ttype=\"button\"\n\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\tdata-target=\"#collapse-4\"\n\t\t\t\taria-expanded=\"false\"\n\t\t\t\taria-controls=\"collapse-4\"\n\t\t\t>\n\t\t\t\tBenchmarks and Competitions\t\t\t<\/button>\n\t\t<\/h4>\n\t\t<div class=\"collapse\" id=\"collapse-4\">\n\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t<p dir=\"ltr\">Dafny was a popular tool among the teams at the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/sites.google.com\/site\/vstte2012\/compet\">VSTTE 2012 program verification competition<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.\u00a0 It was also used at the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/foveoos2011.cost-ic0701.org\/verification-competition\">COST Verification Competition 2011<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, as part of the FoVeOOS conference.\u00a0 And it was used in the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.vscomp.org\/\">VSComp 2010<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> competition at VSTTE 2010, from which a <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/krml214.pdf\">report<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> was published:<\/p>\n<blockquote>\n<p dir=\"ltr\">Vladimir Klebanov, Peter M\u00fcller, Natarajan Shankar, Gary T. Leavens, Valentin W\u00fcstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiss.\u00a0 <strong>The 1st Verified Software Competition: Experience Report<\/strong>.\u00a0 In <em>FM 2011: Formal Methods &#8211; 17th International Symposium on Formal Methods<\/em>, volume 6664 of LNCS, pages 154-168.\u00a0 Springer, 2011.\u00a0 [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/krml214.pdf\">PDF<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>]<\/p>\n<\/blockquote>\n<p dir=\"ltr\">(which\u00a0won\u00a0Best Paper Award at FM 2011).\u00a0 You can find Dafny solutions to the problem sets of these competitions under the Test directory of the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/dafny.codeplex.com\/\">Dafny sources<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n<p dir=\"ltr\">Dafny has also been used to solve various verification benchmark challenges.\u00a0 At the Verified Software: Tools, Techniques, and Experiments (VSTTE 2008) conference, Weide et al. presented some verification benchmarks to facilitate the comparison between different specification languages and verifiers.\u00a0 This paper describes Dafny programs for those benchmarks:<\/p>\n<blockquote>\n<p dir=\"ltr\">K. Rustan M. Leino and Rosemary Monahan.\u00a0 <strong>Dafny meets the Verification Benchmarks Challenge<\/strong>.\u00a0 In <em>VSTTE 2010<\/em>, volume 6217 of LNCS, pages 112-126.\u00a0 Springer, 2010.\u00a0[<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/krml205.pdf\">PDF<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>]<\/p>\n<\/blockquote>\n<p dir=\"ltr\">Dafny has also been used to solve some of the VACID-0 verification benchmarks:<\/p>\n<blockquote>\n<p dir=\"ltr\">K. Rustan M. Leino and Micha\u0142 Moskal.\u00a0 <strong>VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0<\/strong>.\u00a0\u00a0Tools and Experiments workshop at VSTTE\u00a02010. [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2008\/12\/krml209.pdf\">PDF<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>]<\/p>\n<\/blockquote>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\">\n\t\t<h4 class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\ttype=\"button\"\n\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\tdata-target=\"#collapse-5\"\n\t\t\t\taria-expanded=\"false\"\n\t\t\t\taria-controls=\"collapse-5\"\n\t\t\t>\n\t\t\t\tTeaching\t\t\t<\/button>\n\t\t<\/h4>\n\t\t<div class=\"collapse\" id=\"collapse-5\">\n\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t<p dir=\"ltr\">Dafny is being used in teaching.\u00a0 Here&#8217;s a partial list of universities that are or have been using Dafny in some capacity in lectures and class work:<\/p>\n<ul>\n<li>\n<div>Caltech, Rajeev Joshi (<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rjoshi.org\/cs116\/index.html\" target=\"_self\">CS 116<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>)<\/div>\n<\/li>\n<li>\n<div>Lomonosov Moscow State University, Eugene Kornykhin<\/div>\n<\/li>\n<li>\n<div>Kansas State University, Torben Amtoft<\/div>\n<\/li>\n<li>\n<div>Imperial College London, Sophia Drossopoulou and Will Sonnex<\/div>\n<\/li>\n<li>\n<div>NUI Maynooth, Rosemary Monahan<\/div>\n<\/li>\n<li>\n<div>ETH Zurich, Peter M\u00fcller<\/div>\n<\/li>\n<li>\n<div>University of Washington, Ethan Jackson; Emina Torlak<\/div>\n<\/li>\n<li>\n<div>University of Iowa, Cesare Tinelli<\/div>\n<\/li>\n<li>\n<div>Ko\u00e7\u00a0University, Serdar Ta\u015f\u0131ran<\/div>\n<\/li>\n<li>\n<div>Rice University, Swarat Chaudhuri (<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cs.rice.edu\/~sc40\/COMP507\/\" target=\"_self\">COMP 507<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>)<\/div>\n<\/li>\n<li>\n<div>UNSW, Carroll Morgan<\/div>\n<\/li>\n<li>\n<div>University of Toronto, Azadeh Farzan<\/div>\n<\/li>\n<li>\n<div>Princeton, Andrew Appel<\/div>\n<\/li>\n<li>\n<div>CMU, Jonathan Aldrich<\/div>\n<\/li>\n<li>\n<div>Chalmers Technical University, Moa Johansson<\/div>\n<\/li>\n<li>\n<div>Eindhoven Technical University, Kees Huizing<\/div>\n<\/li>\n<li>\n<div>Ohio State University, Bruce Weide<\/div>\n<\/li>\n<li>\n<div>Clemson University, Murali Sitaraman<\/div>\n<\/li>\n<li>\n<div>FCT Universidade Nova de Lisboa, Luis Caires<\/div>\n<\/li>\n<li>\n<div>University of the Basque Country, Paqui Lucio<\/div>\n<\/li>\n<li>\n<div>University of Southampton, Michael Butler<\/div>\n<\/li>\n<li>University of Twente, Marieke Huisman<\/li>\n<li>Yale, Ruzica Piskac<\/li>\n<li>SUNY Stony Brook, Annie Liu<\/li>\n<li>University of Edinburgh, Ian Stark (<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/blog.inf.ed.ac.uk\/apl14\/\/about\" target=\"_self\">APL14<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>)<\/li>\n<li>L\u00fcbeck University of Applied Sciences, Andreas Schaefer<\/li>\n<li>UniBw M\u00fcnchen, Birgit Elbl and Lothar Schmitz<\/li>\n<li>IIT Madras, Ganesan Ramalingam<\/li>\n<li>Clarkson University, Christopher Lynch<\/li>\n<li>Tel Aviv University, Mooly Sagiv<\/li>\n<li>University of Utah, Zvonimir Rakamaric<\/li>\n<li>Memorial University, Theodore Norvell<\/li>\n<li>University of California, Santa Cruz, Cormac Flanagan<\/li>\n<li>Trinity College Dublin, Vasileios Koutavas<\/li>\n<li>Farhad Mehta, HSR Hochschule f\u00fcr Technik Rapperswil<\/li>\n<\/ul>\n<p>and tutorials and summer schools:<\/p>\n<ul>\n<li>Summer School Marktoberdorf, 2008 and 2011<\/li>\n<li>LASER Summer School, 2011<\/li>\n<li>Summer School on Logic and Theorem-Proving in Programming Languages, Eugene, OR, 2008<\/li>\n<li>Tutorial, KTH, Stockholm, 2012<\/li>\n<li>Invited tutorial, VSTTE 2012<\/li>\n<li>Tutorial, HILT 2012<\/li>\n<li>Tutorial, ICSE 2013<\/li>\n<\/ul>\n<p>If you are, or have been, teaching using Dafny, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/leino\/\">Rustan Leino<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> would love to know of your experience. And if you want a mention on these lists, please let him know.<\/p>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\">\n\t\t<h4 class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\ttype=\"button\"\n\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\tdata-target=\"#collapse-6\"\n\t\t\t\taria-expanded=\"false\"\n\t\t\t\taria-controls=\"collapse-6\"\n\t\t\t>\n\t\t\t\tLinks\t\t\t<\/button>\n\t\t<\/h4>\n\t\t<div class=\"collapse\" id=\"collapse-6\">\n\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t<ul>\n<li>Try <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/dafny\/Hello\">Dafny in your browser<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/dafny\/\">Download <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>Dafny<\/li>\n<li>Contribute to Dafny <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/dafny\/\">source<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Dafny <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Dafny\/tutorial\/guide\">online tutorial<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t<\/div>\n\t\n","protected":false},"excerpt":{"rendered":"<p>Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and\u00a0inductive datatypes,\u00a0and builds in specification constructs. The specifications include [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170169","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-12-23","related-publications":[164709],"related-downloads":[],"related-videos":[188098],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Chris Hawblitzel","user_id":31425,"people_section":"Group 1","alias":"chrishaw"},{"type":"user_nicename","display_name":"Jay Lorch","user_id":32732,"people_section":"Group 1","alias":"lorch"},{"type":"user_nicename","display_name":"Michal Moskal","user_id":37431,"people_section":"Group 1","alias":"mimoskal"},{"type":"user_nicename","display_name":"Nikhil Swamy","user_id":33138,"people_section":"Group 1","alias":"nswamy"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170169","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170169\/revisions"}],"predecessor-version":[{"id":477702,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170169\/revisions\/477702"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170169"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170169"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170169"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170169"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170169"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}