What do you think?
Rate this book
Introducing Software Verification with Dafny Language
Get introduced to software verification and proving correctness using the Microsoft Research-backed programming language, Dafny. While some other books on this topic are quite mathematically rigorous, this book will use as little mathematical symbols and rigor as possible, and explain every concept using plain English. It's the perfect primer for software programmers and developers with C# and other programming language skills.
Writing correct software can be hard, so you'll learn the concept of computation and software verification. Then, apply these concepts and techniques to confidently write bug-free code that is easy to understand. Source code will be available throughout the book and freely available via GitHub.
After reading and using this book you'll be able write correct, big free software source code applicable no matter which platform and programming language you use.
What You Will Learn
Discover the Microsoft Research-backed Dafny programming language
Explore Hoare logic, imperative and functional programs
Work with pre- and post-conditions
Use data types, pattern matching, and classes
Dive into verification examples for potential re-use for your own projects
Who This Book Is For
Software developers and programmers with at least prior, basic programming experience. No specific language needed. It is also for those with very basic mathematical experience (function, variables).
Writing correct software can be hard, so you'll learn the concept of computation and software verification. Then, apply these concepts and techniques to confidently write bug-free code that is easy to understand. Source code will be available throughout the book and freely available via GitHub.
After reading and using this book you'll be able write correct, big free software source code applicable no matter which platform and programming language you use.
What You Will Learn
Discover the Microsoft Research-backed Dafny programming language
Explore Hoare logic, imperative and functional programs
Work with pre- and post-conditions
Use data types, pattern matching, and classes
Dive into verification examples for potential re-use for your own projects
Who This Book Is For
Software developers and programmers with at least prior, basic programming experience. No specific language needed. It is also for those with very basic mathematical experience (function, variables).
151 pages, Paperback
Published March 15, 2022
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 1 of 1 review
March 29, 2024
I bought this book because I attended software verification course on university and I want to get some practical look to things which we solved on paper in classroom. For this purpose, book served good. But I am not sure if there are more target audience. Book stays that it mixes little amount of math with Dafny and it is true, but for total beginners it is too little math and for experienced verification engineers there are too little Dafny. Book silently assume previous experiences with university math, programming and especially functional programming. While author use many functional concepts like defining numbers using successor function, for people who never seen it, it may seem crazy and book do not contain any explanation.
The common denominator for most issues is that the book is short. Conclusion ends on page 123 and in comparison with other (Apress) books, form factor is narrower and font is bigger, so I consider it like 80 to 100 pages long in standard form factor.
Book was released in 2022 and in 2024-03 most of the book is still up-to-date, but there are new version of Dafny and few examples do not work. While book at cover says it is good for programmers in "C#, JavaScript, Java, C++, and other programming language", the only non-Dafny code inside is written in Python and I am curious about the former statement. I think it is suitable for every programmer who want to learn mathematical proving of software correctness, no matter of primary language.
The idea of book is good, but result is worse. I give this book 4-star rating because I like the idea of book introducing software verification combining acceptable amount of math with practical programming, but I think this book should be more than twice longer, explain more Dafny features, show solution of exercises (only exercises in chapter 8 has provided correct solutions) and be much more detailed and comprehensive. It is questionable if the book worth the price. If you really want to learn Dafny and software verification, now it seems to me that slightly newer and much more expensive Program Proofs written by K. Rustan M. Leino (978-0262546232) or just a tutorial on Dafny webpage are better sources.
The common denominator for most issues is that the book is short. Conclusion ends on page 123 and in comparison with other (Apress) books, form factor is narrower and font is bigger, so I consider it like 80 to 100 pages long in standard form factor.
Book was released in 2022 and in 2024-03 most of the book is still up-to-date, but there are new version of Dafny and few examples do not work. While book at cover says it is good for programmers in "C#, JavaScript, Java, C++, and other programming language", the only non-Dafny code inside is written in Python and I am curious about the former statement. I think it is suitable for every programmer who want to learn mathematical proving of software correctness, no matter of primary language.
The idea of book is good, but result is worse. I give this book 4-star rating because I like the idea of book introducing software verification combining acceptable amount of math with practical programming, but I think this book should be more than twice longer, explain more Dafny features, show solution of exercises (only exercises in chapter 8 has provided correct solutions) and be much more detailed and comprehensive. It is questionable if the book worth the price. If you really want to learn Dafny and software verification, now it seems to me that slightly newer and much more expensive Program Proofs written by K. Rustan M. Leino (978-0262546232) or just a tutorial on Dafny webpage are better sources.
Displaying 1 - 1 of 1 review