Top 1,000 Features Creators Events Podcasts Extensions Blog Explorer CSV Download

Dafny

< >

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

#228on PLDB 15Years Old 157Repos
Download source code:
git clone https://github.com/Microsoft/dafny

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


Example from Riju:
method Main() { print "Hello, world!\n"; }
// 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 Token Example
Print() Debugging print
Comments
// A comment
Line Comments //
// A comment
Semantic Indentation X

View source

- Build the next great programming language · About · Resources · Acknowledgements · Part of the World Wide Scroll