"Validatable" trait for classes using the Valid()/Repr idiom #22
Conversation
| // A trait for objects with a Valid() predicate. Necessary in order to | ||
| // generalize some proofs, but also useful for reducing the boilerplate | ||
| // that most such objects need to include. | ||
| trait {:termination false} Validatable { |
There was a problem hiding this comment.
Does that mean you're turning off the termination checker for this trait? Termination is an important correctness property, and I wouldn't feel comfortable using a standard library that adds such axioms without clear documentation on why it does so, why it's really needed, and why it's safe.
I haven't thought it through, but did you try to re-enable the termination checker and to prove termination using a decreasing Repr set?
There was a problem hiding this comment.
Ah I wrote this so long ago I got used to seeing that. :) It's not turning off termination checking for this trait nor the classes inheriting it. It's only necessary in order to allow any class to extend this trait at all. This appears to be because allowing a class to extend a trait from a different module introduces unsoundness in the termination checking somehow - I'm only going by the error message here as this attribute doesn't appear to be documented.
This is still a good reason to block on doing better though. I know Rustan's talked about this unsoundness not being hard to fix so we'll at least document it better if not fix it.
There was a problem hiding this comment.
Rustan has kindly provided LOTS of detail on why we have {:termination false}: dafny-lang/dafny#1588 :)
Encapsulates the idiom described in Chapters 8 and 9 of http://leino.science/papers/krml221.pdf as a shared common trait.