Ilmu Komputer & AI editorial
Open AccessOA2026
DSpec2Test: Specification-Driven Test Generation in Dafny
A blackbox, DNF-based approach that outperforms implementation-driven test generation
Sofia Vieira Pinto; Álvaro F. Silva; João Pascoal Faria; Alexandra Mendes· 2026· DOI 10.48550/arXiv.2609.29713
The core problem
Verification-aware languages such as Dafny integrate logical constructs directly into code, enabling automatic verification of program correctness. However, tests remain valuable in scenarios that verification alone does not address, such as supporting test-driven development. Existing Dafny test generation tools are implementation-based, which limits their applicability when specifications are the primary artifact. The authors present DSpec2Test, a specification-driven test generation tool for Dafny that automatically derives tests from formal specifications without considering implementation details. The tool extends Dafny's `generate-tests` command with a new blackbox mode based on Disjunctive Normal Form (DNF) equivalence class partitioning and optional Boundary Value Analysis (BVA). DSpec2Test relies on the Z3 SMT solver to synthesize inputs and expected outputs that meet the specification-derived constraints. The evaluation uses programs from DafnyBench mutated with MutDafny and compares DSpec2Test against Dafny's existing implementation-driven Block mode.
Innovation
The evaluation compares DSpec2Test against Dafny's existing implementation-driven Block mode on a dataset of 131 mutants generated from DafnyBench programs using MutDafny. The primary metric is mutation kill rate. DSpec2Test achieves a 93.9% mutation kill rate, while Block achieves 82.4%. Notably, DSpec2Test uniquely kills 17 mutants that Block does not kill, demonstrating its complementary nature. The results are summarized in the table below:
| Tool | Mutation Kill Rate |
|------|-------------------|
| DSpec2Test | 93.9% |
| Block | 82.4% |
These results suggest that specification-driven testing is an effective and complementary approach for testing Dafny programs. The higher kill rate indicates that deriving tests from specifications can expose faults that implementation-based testing misses, particularly when the implementation deviates from the specification.
Verification-aware languages such as Dafny integrate logical constructs directly into code, enabling automatic verification of program correctness. However, tests remain valuable in scenarios that verification alone does not address, such as supporting test-driven development. Existing Dafny test generation tools are implementation-based, which limits their applicability when specifications are the primary artifact. The authors present DSpec2Test, a specification-driven test generation tool for Dafny that automatically derives tests from formal specifications without considering implementation details. The tool extends Dafny's `generate-tests` command with a new blackbox mode based on Disjunctive Normal Form (DNF) equivalence class partitioning and optional Boundary Value Analysis (BVA). DSpec2Test relies on the Z3 SMT solver to synthesize inputs and expected outputs that meet the specification-derived constraints. The evaluation uses programs from DafnyBench mutated with MutDafny and compares DSpec2Test against Dafny's existing implementation-driven Block mode.
DSpec2Test operates as a blackbox test generator: it takes a Dafny specification (preconditions, postconditions, and invariants) and ignores the implementation body. The core algorithm partitions the input space using DNF equivalence class partitioning. Given a specification, the tool extracts logical constraints and converts them into DNF, where each disjunct represents a distinct equivalence class of inputs that satisfy the same specification branches. For each class, Z3 is queried to synthesize concrete input values and corresponding expected outputs that satisfy the postcondition. Optionally, Boundary Value Analysis (BVA) is applied to generate additional tests at the boundaries of each equivalence class, improving fault detection for off-by-one and edge-case errors. The generated tests are expressed as Dafny test methods that can be executed with the Dafny test runner. The tool is implemented as an extension to Dafny's `generate-tests` command, adding a `--blackbox` mode. The workflow is illustrated below:
Why it matters
The findings highlight the value of specification-driven test generation in verification-aware languages. By focusing on specifications rather than implementations, DSpec2Test supports test-driven development and can be used even before an implementation exists. The use of DNF equivalence class partitioning ensures systematic coverage of specification branches, while optional BVA targets boundary conditions. The reliance on Z3 enables precise synthesis of inputs and expected outputs. The 93.9% mutation kill rate and the unique kills of 17 mutants underscore the complementary role of specification-driven testing alongside implementation-driven approaches. However, the approach may be limited by the complexity of specifications and the scalability of SMT solving. Future work could explore combining both modes, extending to other verification-aware languages, and integrating with continuous integration pipelines. Overall, DSpec2Test represents a significant step toward more effective testing in formal development environments.
Who should read this
CS practitioners and researchers
Opening member content…