Dafny
   HOME

TheInfoList



OR:

Dafny is an imperative and
functional Functional may refer to: * Movements in architecture: ** Functionalism (architecture) ** Form follows function * Functional group, combination of atoms within molecules * Medical conditions without currently visible organic basis: ** Functional sy ...
compiled language A compiled language is a programming language whose implementations are typically compilers (translators that generate machine code from source code), and not interpreters (step-by-step executors of source code, where no pre-runtime translation t ...
that compiles to other
programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...
s, such as C#,
Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's List ...
,
JavaScript JavaScript (), often abbreviated as JS, is a programming language that is one of the core technologies of the World Wide Web, alongside HTML and CSS. As of 2022, 98% of Website, websites use JavaScript on the Client (computing), client side ...
, Go and
Python Python may refer to: Snakes * Pythonidae, a family of nonvenomous snakes found in Africa, Asia, and Australia ** ''Python'' (genus), a genus of Pythonidae found in Africa and Asia * Python (mythology), a mythical serpent Computing * Python (pro ...
. It supports
formal specification In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verif ...
through preconditions,
postconditions In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions wit ...
,
loop invariant In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked within the code by an assertion call. Knowing its invariant(s) is essential in und ...
s,
loop variant In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some inva ...
s, termination specifications and read/write framing specifications. The language combines ideas from the
functional Functional may refer to: * Movements in architecture: ** Functionalism (architecture) ** Form follows function * Functional group, combination of atoms within molecules * Medical conditions without currently visible organic basis: ** Functional sy ...
and imperative paradigms; it includes support for
object-oriented programming Object-oriented programming (OOP) is a programming paradigm based on the concept of "objects", which can contain data and code. The data is in the form of fields (often known as attributes or ''properties''), and the code is in the form of pr ...
. Features include ''generic classes'', ''dynamic allocation'', ''inductive datatypes'' and a variation of
separation logic In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion l ...
known as ''implicit dynamic frames'' for reasoning about side effects. Dafny was created by Rustan Leino at
Microsoft Research Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technologi ...
after his previous work on developing ESC/Modula-3,
ESC/Java ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extend ...
, and Spec#. Dafny is widely used in teaching because it provides a simple, integrated introduction to formal specification and verification; it is regularly featured in software verification competitions (e.g. VSTTE'08, VSCOMP'10, COST'11, and VerifyThis'12). Dafny was designed as a verification-aware programming language, requiring verification along with code development. It thus fits the "Correct 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 of
Hoare logic Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
. Dafny builds on the Boogie
intermediate language An intermediate representation (IR) is the data structure or code used internally by a compiler or virtual machine to represent source code. An IR is designed to be conducive to further processing, such as optimization and translation. A "good ...
which uses the Z3 automated theorem prover for discharging proof obligations.


Data types

Dafny provides methods for implementation which may have
side-effects In medicine, a side effect is an effect, whether therapeutic or adverse, that is secondary to the one intended; although the term is predominantly employed to describe adverse effects, it can also apply to beneficial, but unintended, consequence ...
and functions for use in specification which are
pure Pure may refer to: Computing * A pure function * A pure virtual function * PureSystems, a family of computer systems introduced by IBM in 2012 * Pure Software, a company founded in 1991 by Reed Hastings to support the Purify tool * Pure-FTPd, F ...
. 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 < arr.Length

> max >= arr // Return must match some element in array ensures exists j : int :: j>=0 && j < arr.Length && max

arr
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 Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
. 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 example illustrates using loops: method sumAndZero(arr: array) returns (sum: nat) requires forall i :: 0 <= i < arr.Length

> arr >= 0 modifies arr
This fails verification because Dafny cannot establish that (sum + arr >= 0 holds at the assignment. From the precondition, intuitively, forall i :: 0 <= i < arr.Length

> arr >= 0
holds in the loop since arr := arr 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 := arr ; or (b) add the loop invariant invariant forall i :: 0 <= i < arr.Length

> arr >= 0
Dafny additionally employs limited
static analysis Static analysis, static projection, or static scoring is a simplified analysis wherein the effect of an immediate change to a system is calculated without regard to the longer-term response of the system to that change. If the short-term effect i ...
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 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 In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
. 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 In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
, 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 predicate isNatList(l: List) lemma NatSumLemma(l: List, n: int) requires isNatList(l) && n

sum(l) ensures n >= 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 Structural induction is a proof method that is used in mathematical logic (e.g., in the proof of Łoś' theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural num ...
). 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 Access modifiers (or access specifiers) are keywords in object-oriented languages that set the accessibility of classes, methods, and other members. Access modifiers are a specific part of programming language syntax used to facilitate the enca ...
. 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


Further reading

* *


External links


Dafny: A Language and Program Verifier for Functional Correctness - Microsoft ResearchGitHub - dafny-lang/dafny: Dafny is a verification-aware programming language
{{Microsoft Research 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