Dafny is an imperative programming language that allows software to be verified through preconditions, postconditions, and invariants. Designed by Rustan Leino and developed by Microsoft since 2009, Dafny is used in academia and the industry and is regularly used in software verification competitions.
As a programming language, Dafny shares many features with languages from the “imperative” family or paradigm, such as C, C++, and Java. There are functions and procedures (methods), ...
Get Introducing Software Verification with Dafny Language: Proving Program Correctness now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
Get Mark Richards’s Software Architecture Patterns ebook to better understand how to design components—and how they should interact.
Dive in for free with a 10-day trial of the O’Reilly learning platform—then explore all the other resources our members count on to build skills and solve problems every day.
Start your free trial Become a member now