Skip to content

Commit

Permalink
Minor fix
Browse files Browse the repository at this point in the history
  • Loading branch information
Dargones authored Nov 1, 2023
1 parent 1a17e44 commit 67998d6
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ title: "Automated Test Generation: Chess Puzzles with Dafny"
date: 2023-11-10 11:00:00 -0500
author: Sasha Fedchin
---
Dafny is incredibly powerful. With it, you can prove [type safety properties of a programming language](https://dafny.org/blog/2023/07/14/types-and-programming-languages/), you can [verify runtime complexity of well-known algorithms](https://dafny.org/blog/2023/10/11/insertion-sort/), you can [identify conflicting specifications](https://dafny.org/blog/2023/10/27/proof-dependencies/), and [much more](https://dafny.org/blog/). In many cases, verification provides all the correctness guarantees that you need for your project. However if, like a number of industrial Dafny users, you want to integrate Dafny code with existing codebases, you may face challenges that verification alone might not solve and where runtime testing could be useful:
Dafny is incredibly powerful. With it, you can prove [type safety properties of a programming language](https://dafny.org/blog/2023/07/14/types-and-programming-languages/), you can [verify runtime complexity of an algorithm](https://dafny.org/blog/2023/10/11/insertion-sort/), you can [identify conflicting specifications](https://dafny.org/blog/2023/10/27/proof-dependencies/), and [much more](https://dafny.org/blog/). In many cases, verification provides all the correctness guarantees that you need for your project. However if, like a number of industrial Dafny users, you want to integrate Dafny code with existing codebases, you may face challenges that verification alone might not solve and where runtime testing could be useful:

- Your code is actually a reference implementation for another program, and you want to test the equivalence between the two.
- 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.
Expand Down

0 comments on commit 67998d6

Please sign in to comment.