search

dafny-lang / dafny

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

Distinguish good Dafny examples from regression tests #2788

Open robin-aws opened 1 year ago

robin-aws commented 1 year ago

There are a lot of excellent examples of small Dafny programs in the regression suite under Test. However, the regression suite's primary goal is good testing coverage for the set of all possible Dafny programs, not just well-written ones. By design we will need to include code we wouldn't recommend anyone write currently, including deprecated features and discouraged idioms.

I would suggest we find a way to make this distinction clearer, either by moving good examples to a separate area still included in the regression suite, or perhaps the opposite approach of flagging tests that aren't good examples somehow.

Potentially related to #2679. CC @davidcok

atomb commented 1 year ago

I'm strongly in favor of a top-level Examples directory that includes nice examples, along with motivating documentation (and that, of course, is also included in the test process). The first candidates for inclusion in that directory might be some of the things currently in Test.