Dafny Documentation

The XUnitExtensions package provides specialized extensions for the xUnit testing framework, specifically designed to handle complex test scenarios that standard xUnit features do not support natively. It offers two primary capabilities:

1. File-encoded Parameterized Theory Tests: Enables parameterized Theory tests where each test case is represented by an individual file. This approach allows for parallel execution of test cases within a single theory and supports sharding test cases across multiple machines.
2. LIT Test Interpreter: Provides an alternate interpreter for LLVM Integrated Tester (LIT) tests, allowing test suites written in LIT syntax to be executed as xUnit Theory tests.

Dafny is an imperative, sequential programming language designed for static verification. It supports generic classes, inheritance, abstraction, methods, functions, dynamic allocation, and inductive/coinductive datatypes.

Key verification features include:

• Specifications: Pre-conditions, post-conditions, frame specifications (read/write sets), and termination metrics.
• Ghost Constructs: Ghost variables and specification constructs used only during verification; these are omitted from the final executable code.
• Verification Engine: Powered by Boogie and Z3.
• Compilation Backends: The dafny compiler can produce code for .NET (via C#), Java, JavaScript, Go, and C++, each providing a Foreign Function Interface (via :extern) and a runtime library.

Dafny is a verification-ready programming language that allows you to write both code and specifications in the same language. It supports:

Programming Concepts

• Classes and Trait Inheritance
• Inductive Datatypes: Suitable for pattern matching and containing methods.
• Lazily Unbounded Datatypes (Co-inductive datatypes).
• Subset Types: e.g., for bounded integers.
• Lambdas
• Data Structures: Both immutable and mutable.

Mathematical Proof Toolbox

• Quantifiers: Unbounded and bounded.
• Calculational Proofs
• Specification Clauses: Pre-conditions, post-conditions, termination conditions, loop invariants, and read/write specifications.

Compilation Targets

Compiled code can be integrated into existing workflows by targeting:

• C#
• Go
• Python
• Java
• JavaScript

The Std.Wrappers module provides simple datatypes to support common patterns like optional values or operations that can fail. These types are designed to work seamlessly with Dafny's update-with-failure :- operator.

To use these types, import the module:

import opened Std.Wrappers

Supported failure-compatible (FC) types:

• Option<R>: Either Some with a value of type R or None.
• Outcome<E>: Either Pass (no information) or Fail with an error value of type E.
• Result<R,E>: Either Success with a value of type R or Failure with an error value of type E.

TestDafny (also known as %testdafny) is an internal testing utility designed to execute a single Dafny source file against multiple compile target options. It asserts that the output matches the corresponding <test file>.expect file.

This utility is useful for ensuring consistency across different backends and is used to generate the compiler feature support matrix in the Dafny reference manual.

Specifications in Dafny describe the logical properties of methods, functions, lambdas, iterators, and loops. They are used to define preconditions, postconditions, invariants, memory access permissions (read/modify), and termination information.

Specifications are implemented using specification clauses. These clauses:

• Typically appear in a sequence.
• Begin with a specific keyword.
• Do not end with semicolons.

Specifications are applied at different levels:

1. Specification Clauses: The individual building blocks (e.g., RequiresClause).
2. Entity Specifications: A sequence of clauses applied to an entity (e.g., MethodSpec).
3. Entity Declarations: The top-level declaration that includes the specifications (e.g., MethodDecl).

Dafny expressions are categorized into three types based on their behavior and allowed usage:

1. Standard Expressions: Most expressions have no side-effects and can be used in methods, functions, specifications, and either compiled or ghost code.
2. Right-hand-side (RHS) Expressions: These have side-effects (e.g., object allocation, method calls) and are restricted to specific locations, typically the right-hand side of update (assignment) statements. Note that while method calls and function calls are syntactically similar, method calls are semantically restricted to RHS locations.
3. Specification Expressions: These are restricted exclusively to specifications and other ghost code.