Details

Autor(en) / Beteiligte

• Fedchin, Aleksandr
• Dean, Tyler
• Foster, Jeffrey S.
• Mercer, Eric
• Rakamarić, Zvonimir
• Reger, Giles
• Rungta, Neha
• Salkeld, Robin
• Wagner, Lucas
• Waldrip, Cassidy
• Rozier, Kristin Yvonne
• Chaudhuri, Swarat

Titel

A Toolkit for Automated Testing of Dafny

Ist Teil von

• NASA Formal Methods, 2023, Vol.13903, p.397-413

Ort / Verlag

Switzerland: Springer

Erscheinungsjahr

2023

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Dafny is a verification-ready programming language that is executed via compilation to C# and other mainstream languages. We introduce a toolkit for automated testing of Dafny programs, consisting of DUnit (unit testing framework), DMock (mocking framework), and DTest (automated test generation). The main component of the toolkit, DTest, repurposes the Dafny verifier to automatically generate DUnit test cases that achieve desired coverage. It supports verification-specific language features, such as pre- and postconditions, and leverages them for mocking with DMock. We evaluate the new toolkit in two ways. First, we use two open-source Dafny projects to demonstrate that DTest can generate unit tests with branch coverage that is comparable to the expectations developers set for manually written tests. Second, we show that a greedy approach to test generation often produces a number of tests close to the theoretical minimum for the given coverage criterion.