search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.87k stars 255 forks source link

Questions on test generation #1720

Open hmijail opened 2 years ago

hmijail commented 2 years ago

I'm looking for ways to test Dafny code, found the test generation page and have a few questions that I'm hoping you could answer:

  1. The release notes for Dafny 3.3 mention "a facility for generating test input" - is this the same?
  2. The test generation page talks about (unit) tests, yet it doesn't test anything, probably because of the mentioned missing oracle. Given the explanation of the existing functionality and the examples, my understanding is that this is rather like a verifier-driven fuzzer that generates small programs that exercise all the code blocks/paths; those programs might then be used to actually do unit testing or whatever else. Is that characterization correct? Am I missing something?
  3. Dead code detection is the first stated purpose, though actually it seems totally disconnected from the "testing" subject. Even the CLI call in the example doesn't use any of the /generateTest options. I'm guessing that the connection to test generation is just the underlying "fuzzing" / path detection machinery - is that correct?
  4. How does this "test generation" help with "testing the implementation of unverified external methods"? Is it just about exercising those external methods to coax errors out?
  5. Similarly, how does this help with comparing implementations in Dafny and other language? Is the idea to have interface-compatible implementations in Dafny and another language, and then run the generated tests against both, comparing their results?
  6. Given the explanations in the page and the suggestion in dafny /help, I'd guess that to always add /definiteAssignment:3 is helpful and brings no harm for test generation and dead code detection. But then, why not make it an internal default for those?
hmijail commented 2 years ago
  1. "Dead code" is used as synonymous to "unreachable code". But, given the explanation of needing a Boogie implementation, does this really mean something like "code ignored by the verifier"?
hmijail commented 1 year ago

Bumping this old issue. I notice that the README.md file was updated on July 2022, which kinda answered questions 4 and 5. But the others remain...

Dargones commented 1 year ago

Apologies for missing this issue, @hmijail... Test Generation just got upgraded as of Dafny 4.0 so I will answer the questions above based on the new version. Please feel free to ping me about any test generation and counterexample extraction issues! 1) Yes 2) Generated tests now include oracles that are extracted from non-ghost post-conditions. 3) Yes, test generation and dead code identification share the same mechanism under the hood. The distinction is made in case there would be other ways of detecting dead code in the future 4) At the moment, yes, testing helps to exercise external methods only indirectly. 5) Yes, that would be the idea. 6) Done. The CLI has changed a lot recently in general, you can now simply run dafny generate-tests and get a dedicated help message 7) I think "unreachable code" would be the best term since the tool will report Boogie blocks that, if you put an assert false in them, will not verify.