The Howdy Glossary

Dafny is a programming language with an integrated development environment that supports formal verification. The language uses inductive assertions and allows for modular reasoning, making it easier to write correct code by construction. Dafny programs are annotated with pre- and post-conditions, loop invariants, and method contracts. The Dafny IDE verifies these annotations using an automated theorem prover called Z3. It produces counterexamples when verification fails. Dafny is frequently used for teaching the principles of program correctness and has also found applications in research projects where highly reliable software is necessary.