Dafny - Programming language

Dafny is an open source programming language created in 2009 by K. Rustan M. Leino.

#216on PLDB

15Years Old

157Repos

Download source code:

git clone https://github.com/Microsoft/dafny

Homepage · REPL · Try It Online · Source Code · Wikipedia

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...

Tags: programming language
Dafny is developed on GitHub and has 2,853 stars
There are at least 157 Dafny repos on GitHub
Early development of Dafny happened in Microsoft
Dafny is written in C#, Markdown, Java, YAML, F#, TOML, Python, Go, XML, HTML, Make, Bash, JavaScript, Tex, Bourne shell, Gradle, CSS, JSON, Rust, Diff, SVG
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, Apache Spark, Idris, Agda

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

Language features

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