Adding specs for traits and trait impl blocks. Addresses #41 #71
Conversation
…the trait definition, and to test default method implementations
…aces in the output
|
This is looking pretty good, thanks for working on it! |
Tweaks from code review (mostly format and renames) Co-authored-by: Máté Kovács <481354+mkovaxx@users.noreply.github.com>
| #[spec( | ||
| maintains: self.0 == 3, | ||
| ensures: *output > self.0, | ||
| )] |
There was a problem hiding this comment.
On a second thought, I'm conflicted about the idea of allowing per-method specs inside a trait impl. It feels strange as an idea, but I have a difficult time unpacking why.
There was a problem hiding this comment.
I'm pretty convinced we want both.
Specs on the trait items in the declaration enforce the interface is being upheld, but can't see into the implementation. Specs on the implementation can enforce invariants that must be maintained to ensure the implementation is correct.
There was a problem hiding this comment.
I think we've hit an important question here, so let's move this discussion to the feature's design:
#41 (comment)
…ute on trait or impl block
…a `requires`, `maintains`, or `ensures` directive
Adding span to Spec type
2 participants
Adds spec attributes for traits and trait impl blocks. Addresses #41