search

dafny-lang / dafny

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

Add regression tests for all signatures created by code generators #5715

Open keyboardDrummer opened 2 months ago

keyboardDrummer commented 2 months ago

We should add regression tests that compare the output of dafny translate to a fixed expectation output. However, to allow implementation details, such as method bodies, to change, we should add a hidden option --only-signatures to dafny translate that will prevent it from emitting those details.

robin-aws commented 2 months ago

It might be easier and more effective to expand the scope of https://github.com/dafny-lang/dafny/blob/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy, which is testing for this by literally trying to execute consuming code built with a previous version. If we run that for all backends, and expand the library to cover as many kinds of Dafny declarations as possible, we'll have the same testing coverage without having to implement --only-signatures, and arguably matching the actual requirement better.

keyboardDrummer commented 2 months ago

If we run that for all backends, and expand the library to cover as many kinds of Dafny declarations as possible, we'll have the same testing coverage without having to implement --only-signatures, and arguably matching the actual requirement better.

Somehow that feels complicated to me, although indeed you won't have to implement --only-signatures. One thing you'd have to do is somewhat arbitrarily pick a particular old version to test against, and in theory you might make a change that works for that particular old version, but not for another old version, so it could be less safe. Also, there might be changes that do not cause issues with the particular consuming project you're testing with, but would with another one.

Suppose you make a rather harmless change that adds a new method, but that causes issues with 0.001% of Dafny codebases: only those that contain a particular pattern. Without API diff tests, you might not realize that you even made a change.