Skip to content

Commit

Permalink
chore: address dafny-lang/dafny#2500 (#599)
Browse files Browse the repository at this point in the history
  • Loading branch information
texastony authored Jul 27, 2022
1 parent 398c7f6 commit 686d34b
Showing 1 changed file with 17 additions and 0 deletions.
17 changes: 17 additions & 0 deletions .github/PULL_REQUEST_TEMPLATE.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,20 @@


By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

# Due to [dafny-lang/dafny#2500](https://github.com/dafny-lang/dafny/issues/2500), Traits are dangerous:
1. [ ] Does this PR add any traits or classes that extend a trait?
2. [ ] Are these traits annotated with `{:termination false}`?

The override checks on
the specifications on
a class' functions/methods/etc. validating
that specifications are
at least as strong as those on
the traits it implements
are not working correctly when
that trait is defined in a different module
(and hence must have `{:termination false}` on it).

As such, if either (1.) or (2.) is true:
- [ ] manually verified all the trait specifications are copied onto classes that extend them?

0 comments on commit 686d34b

Please sign in to comment.