Top 1K Features Creators Events Podcasts Books Extensions Interviews Blog Explorer CSV

Dafny

< >

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

#211on 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...


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 Example Token
Print() Debugging ✓ print
Comments ✓ // A comment
Line Comments ✓ // A comment //
Semantic Indentation X
View source
- Build the next great programming language · About · Search · Keywords · Livestreams · Labs · Resources · Acknowledgements · Part of the World Wide Scroll