Dafny Reference Documentation#
Abstract: This is the Dafny reference manual; it describes the Dafny programming language and how to use the Dafny verification system. Parts of this manual are more tutorial in nature in order to help the user understand how to do proofs with Dafny.
(Link to current document as html)
Language reference for the Dafny type system, which also describes available expressions for each type
- 1. Introduction
- 2. Lexical and Low Level Grammar
- 3. 3. Programs (grammar) {#sec-program}
- 4. 4. Modules (grammar) {#sec-modules}
- 5. 5. Types {#sec-types}
- 6. 6. Member declarations {#sec-member-declaration}
- 7. 7. Specifications {#sec-specifications}
- 8. 8. Statements (grammar) {#sec-statements}
- 9. 9. Expressions {#sec-expressions}
- 10. 10. Refinement {#sec-module-refinement}
- 11. 11. Attributes {#sec-attributes}
- 12. 12. Advanced Topics {#sec-advanced-topics}
- 13. Dafny User’s Guide
- 14. 14. Dafny VSCode extension and the Dafny Language Server {#sec-dafny-language-server-vscode}
- 15. 15. Plugins to Dafny {#sec-plugins}
- 16. 16. Full list of legacy command-line options {#sec-full-command-line-options}
- 17. Dafny Grammar
- 18. 18. Testing syntax rendering
- 19. References