DSpec2Test: Specification-Driven Test Generation in Dafny
DSpec2Test is presented, a specification-driven test generation tool for Dafny that automatically derives tests from formal specifications, without considering implementation details, and achieves a 93.9% mutation kill rate on a dataset of 131 mutants, outperforming Block's 82.4%, and uniquely killing 17 mutants.