Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature request: support {:termination false} on classes as well as traits #4642

Open
robin-aws opened this issue Oct 11, 2023 · 0 comments
Open
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking

Comments

@robin-aws
Copy link
Member

This trait is currently only supported on traits, but it would be very easy to also look for it on classes extending traits in other modules. The advantage would be being able to leave the attribute off of traits in shared libraries, such that users of such libraries would receive the error about termination checking being unsound in the presence of dynamic dispatch (#1588), and have to explicitly opt in to this in their code, as opposed to library authors opting in on their reusable traits and hiding this problem from users.

@robin-aws robin-aws added this to the Dafny Standard Libraries milestone Oct 11, 2023
@robin-aws robin-aws added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator) part: resolver Resolution and typechecking and removed part: verifier Translation from Dafny to Boogie (translator) labels Oct 11, 2023
@robin-aws robin-aws self-assigned this Nov 5, 2023
@robin-aws robin-aws removed this from the Dafny Standard Libraries milestone Nov 13, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
Projects
None yet
Development

No branches or pull requests

1 participant