In addition to a verification engine to check implementation against specifications, the Dafny ecosystem includes several compilers, plugins for common software development IDEs, a LSP-based Language Server, a code formatter, a reference manual, tutorials, power user tips, books, the experiences of professors teaching Dafny, and the accumulating expertise of industrial projects using Dafny.
Dafny has support for common programming concepts such as
- mathematical and bounded integers and reals, bit-vectors, classes, iterators, arrays, tuples, generic types, refinement and inheritance,
- inductive datatypes that can have methods and are suitable for pattern matching,
- lazily unbounded datatypes,
- subset types, such as for bounded integers,
- lambda expressions and functional programming idioms,
- and immutable and mutable data structures.
Dafny also offers an extensive toolbox for mathematical proofs about software, including
- bounded and unbounded quantifiers,
- calculational proofs and the ability to use and prove lemmas,
- pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.