一句话：提出从 Dafny 形式规约自动派生黑盒测试的工具，基于 DNF 等价类划分与边界值分析，显著提升变异杀死率。
验证感知语言（如 Dafny）将逻辑构造融入代码并支持自动验证程序正确性，但测试在验证无法覆盖的场景（如测试驱动开发）中仍有价值。然而现有 Dafny 测试生成工具均基于实现，限制了其在此类场景的适用性。本文提出 DSpec2Test，一个面向 Dafny 的规约驱动测试生成工具，可以从形式规约自动派生测试而不考虑实现细节。该工具扩展了 Dafny 的 generate-tests 命令，新增基于析取范式（DNF）等价类划分的黑盒模式，并可选用边界值分析（BVA）；同时借助 Z3 SMT 求解器合成满足规约派生约束的输入与期望输出。作者在经 MutDafny 变异的 DafnyBench 程序上评估 DSpec2Test，并与 Dafny 现有基于实现的 Block 模式对比：在 131 个变异体上，DSpec2Test 的变异杀死率达到 93.9%，优于 Block 的 82.4%，并额外独有杀死 17 个变异体。结果表明规约驱动测试是测试 Dafny 程序的一种有效且互补的方法。
Verification-aware languages, such as Dafny, integrate logical constructs into code and enable automatic verification of program correctness. However, tests remain helpful in scenarios that verification alone does not address (e.g., to support test-driven development). Existing Dafny test generation tools are implementation-based, limiting their applicability in this context. We present DSpec2Test, a specification-driven test generation tool for Dafny that automatically derives tests from formal specifications, without considering implementation details. Our tool extends Dafny's generate-tests command with a new black-box 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. We evaluate DSpec2Test on programs from DafnyBench mutated using MutDafny and compare it against Dafny's existing implementation-driven Block mode. DSpec2Test achieves a 93.9% mutation kill rate on a dataset of 131 mutants, outperforming Block's 82.4%, and uniquely killing 17 mutants. These results suggest that specification-driven testing is an effective and complementary approach for testing Dafny programs. Demo: https://youtu.be/mK1EeJfinRQ Code: https://github.com/VeriFixer/DSpec2Test Prebuilt docker image: https://doi.org/10.5281/zenodo.21191158