Dafny

Dafny is a programming language created in 2009 by K. Rustan M. Leino.

#281on PLDB	14Years Old	2.4kUsers
1Books	11Papers	157Repos

Try now: Riju · TIO

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 for reasoning about side effects. Read more on Wikipedia...

Dafny website
Dafny Wikipedia page
Dafny is developed on GitHub and has 1,714 stars
There are at least 157 Dafny repos on GitHub
Dafny first developed in Microsoft
file extensions for Dafny include dfy
Dafny is written in C#
The Google BigQuery Public Dataset GitHub snapshot shows 1 users using Dafny in 1 repos on GitHub
Explore Dafny snippets on Rosetta Code
Dafny Ubuntu package
Dafny appears in the Quine Relay project
See also: (5 related languages)C#, Spec Sharp, SPARK, Idris, Agda
HTML of this page generated by LanguagePage.ts

Example from Riju:

method Main() {
  print "Hello, world!\n";
}

Example from the Hello World Collection:

// Hello world in Dafny

method Main() {
  print "Hello, World!\n";
}

Example from Wikipedia:

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;
    }
}

Feature	Supported	Token	Example
Print() Debugging	✓	print
Comments	✓		// A comment
Line Comments	✓	//	// A comment
Semantic Indentation	X

title	authors	year	citations	influentialCitations
The Dafny Integrated Development Environment	K. Leino and Valentin Wüstholz	2014	52	2
Developing verified programs with Dafny	K. Leino	2012	42	5
Accessible Software Verification with Dafny	K. Leino	2017	27	1
Developing verified programs with Dafny	K. Leino	2012	9	0
Tactics for the Dafny Program Verifier	G. Grov and V. Tumas	2016	8	0
Automatic verification of Dafny programs with traits	Reza Ahmadi and K. Leino and J. Nummenmaa	2015	6	0
Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny	Sylvia Grewe and Sebastian Erdweg and M. Mezini	2017	4	0
A Tutorial on Using Dafny to Construct Verified Software	P. Lucio	2017	2	0
Towards progressive program verification in Dafny	Ismael Figueroa and Bruno García and Paul Leger	2018	2	0
An Assertional Proof of Red–Black Trees Using Dafny	R. Peña	2019	2	0
Mechanised Verification Patterns for Dafny	G. Grov and Yuhui Lin and V. Tumas	2016	1	0

Dafny - Programming language

Language features

Books about Dafny from ISBNdb

Publications about Dafny from Semantic Scholar