Skip to content

Commit

Permalink
Fix typo (#36)
Browse files Browse the repository at this point in the history
  • Loading branch information
atomb authored Jul 31, 2024
1 parent b1559cc commit 6069d9b
Showing 1 changed file with 2 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Dafny is incredibly powerful. With it, you can prove [type safety properties of
- You are using Dafny's foreign function interface, which allows implementing specifications in languages other than Dafny. Dafny can not verify such external implementations, so you want to test them at runtime to still gain confidence in their correctness.
- You have written a specification for your program and are about to embark on a proof but want to have some initial assurance that your yet-to-be-verified implementation does indeed conform to this specifications.

The following sections explain how Dafny’s built-in automated test generation functionality can help in situations like these. I will use the game of chess as an example and will prompt the test generation toolkit to idenify chess board states that satisfy a given condition, such as a king being under check. The generated tests contain the board states, while the condition is defined by the Dafny program under consideration. A brute force enumeration or fuzzing might not be up to the task here, since the number of ways in which you can arrange pieces on the board is astronomically high. Dafny, however, can use the verifier to generate tests and is, therefore, much more efficient in finding solutions.
The following sections explain how Dafny’s built-in automated test generation functionality can help in situations like these. I will use the game of chess as an example and will prompt the test generation toolkit to identify chess board states that satisfy a given condition, such as a king being under check. The generated tests contain the board states, while the condition is defined by the Dafny program under consideration. A brute force enumeration or fuzzing might not be up to the task here, since the number of ways in which you can arrange pieces on the board is astronomically high. Dafny, however, can use the verifier to generate tests and is, therefore, much more efficient in finding solutions.

The post is structured as follows: I will first outline a [subset of chess rules using Dafny](#1-modelling-chess-in-dafny). This code serves as a reference point throughout the post. I then demonstrate [the basics of test generation](#2-test-generation-basics) and discuss the different coverage metrics you can target. Using this functionality, Dafny users can [visualize coverage and identify dead code](#3-there-is-dead-code-here). Moving on to advanced features, this post offers a [broader discussion of quantifiers, loops and recursion](#sec-quantifiers-loops-and-recursion) — features that require special care when attempting to generate tests. Finally, this blogpost concludes with a [summary and general guidelines](#conclusions-and-best-practices) for how to apply this technique to your own Dafny programs. You can also find more information on automated test generation in the [Dafny reference manual](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dafny-generate-tests). If you want to try test generation on your own, I recommend using Dafny 4.4 or greater, once it is released, and before that the latest Dafny nightly release.

Expand Down Expand Up @@ -277,4 +277,4 @@ Thank you to the Dafny and Boogie developers for their invaluable feedback on th
Thank you to the users of Dafny and the test generation tool in particular, who are a key motivation behind this project: Ryan Emery, Tony Knapp, Cody Roux, Horacio Mijail Anton Quiles, William Schultz, and Serdar Tasiran.

<link rel="stylesheet" href="/blog/assets/css/verification-compelling.css">
<script src="/blog/assets/js/verification-compelling-verification-steps.js"></script>
<script src="/blog/assets/js/verification-compelling-verification-steps.js"></script>

0 comments on commit 6069d9b

Please sign in to comment.