Dafny is an actively used programming language created in 2009. 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...

11Years Old 1,101Users ?Jobs

Example code from the Hello World Collection:

// Hello world in Dafny

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

Example code 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
      // Check what known by Dafny
      assert data >= 0;

Last updated August 9th, 2020

Edit Dafny on GitHub