DSpec2Test：Dafny 中的规范驱动测试生成

中文摘要 AI 辅助

验证感知语言（如 Dafny）将逻辑构造集成到代码中，并能够自动验证程序正确性。然而，在仅靠验证无法解决的场景中（例如，支持测试驱动开发），测试仍然是有帮助的。现有的 Dafny 测试生成工具是基于实现的，限制了它们在此场景中的适用性。我们提出了 DSpec2Test，一个用于 Dafny 的规范驱动测试生成工具，它自动从形式规范中派生测试，而不考虑实现细节。我们的工具扩展了 Dafny 的 generate-tests 命令，新增了一种基于析取范式（DNF）等价类划分和可选边界值分析（BVA）的黑盒模式。DSpec2Test 依赖 Z3 SMT 求解器来合成满足规范派生约束的输入和预期输出。我们使用 MutDafny 对 DafnyBench 中的程序进行变异，评估了 DSpec2Test，并将其与 Dafny 现有的基于实现的 Block 模式进行了比较。DSpec2Test 在包含 131 个变异体的数据集上达到了 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 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. 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.

发表机构

• INESC TEC, Faculdade de Engenharia, Universidade do Porto（波尔图大学工程科学学院）

机构由 AI 辅助整理，请以论文原文为准。