Dafny

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

Source code:

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

#275on PLDB

15Years Old

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

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

Dafny - Programming language

Language features