Questions Concepts
GitHub icon

Dafny

Dafny - Programming language

< >

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


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 · Search · Add Language · Features · Creators · Resources · About · Blog · Acknowledgements · Queries · Stats · Sponsor · Traffic · Traffic Today · Day 305 · feedback@pldb.com · Logout