PLDB
Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon

Dafny

Dafny

Dafny is a pl created in 2009 by K. Rustan M. Leino.

#263on PLDB 13Years Old 2.4kUsers
1Books 11Papers 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"; }
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; } }

Language features

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

Books about Dafny from ISBNdb

title authors year publisher
Introducing Software Verification with Dafny Language: Proving Program Correctness Sitnikovski, Boro 2022 Apress

Publications about Dafny from Semantic Scholar

title authors year citations influentialCitations
The Dafny Integrated Development Environment K. Leino and Valentin Wüstholz 2014 52 2
Developing verified programs with Dafny K. Leino 2012 42 5
Accessible Software Verification with Dafny K. Leino 2017 27 1
Developing verified programs with Dafny K. Leino 2012 9 0
Tactics for the Dafny Program Verifier G. Grov and V. Tumas 2016 8 0
Automatic verification of Dafny programs with traits Reza Ahmadi and K. Leino and J. Nummenmaa 2015 6 0
Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny Sylvia Grewe and Sebastian Erdweg and M. Mezini 2017 4 0
A Tutorial on Using Dafny to Construct Verified Software P. Lucio 2017 2 0
Towards progressive program verification in Dafny Ismael Figueroa and Bruno García and Paul Leger 2018 2 0
An Assertional Proof of Red–Black Trees Using Dafny R. Peña 2019 2 0
Mechanised Verification Patterns for Dafny G. Grov and Yuhui Lin and V. Tumas 2016 1 0
bpmn.html · dafny.html · batch.html

View source

PLDB - Build the next great programming language · v2022 · Day 33 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub · feedback@pldb.com