Implements an {:expect} attribute on an assert statement, which makes it compiled, if not ghost, as well as verified #3458
Conversation
davidcok
changed the title
There was a problem hiding this comment.
Absolutely love this feature, thanks for pushing for it!
Two slight reservations:
- Everywhere we currently use
expect, such as:- expect ..., it's a keyword. Here we're using it as an attribute, which feels inconsistent. - I also find it doesn't read as naturally to use the same word as a modifier as opposed to a direct verb. I wonder if
assert {:checked} Pwould flow better, even though we lose the direct connection to theexpectstatement.
We could even consider assert expect P;, although that also looks odd to me.
| @@ -0,0 +1,10 @@ | |||
| // RUN: %baredafny run --no-verify --use-basename-for-filename "%s" > "%t" | |||
There was a problem hiding this comment.
Rather than just --use-basename-for-filename, most tests that use %baredafny use %args instead.
There was a problem hiding this comment.
Ah. And the reason I forgot to use it is that %args does not play well with 'run' and other such verbs
| @@ -623,6 +623,11 @@ method doSplitHere(x: bool) returns (y: int) { | |||
| ### 23.3.3. `{:subsumption n}` | |||
| Overrides the `/subsumption` command-line setting for this assertion. | |||
|
|
|||
| ### 23.3.4. `{:expect s}` | |||
There was a problem hiding this comment.
For the future, it seems like we could also support adding this to other specification contexts like requires, ensures, invariant, etc. (although see my independent question about whether this is the name we want)
There was a problem hiding this comment.
Despite my slack comment, I see your point. I'm open to any naming, but making it anything other than an attribute would be more work and harder to generalize.
There was a problem hiding this comment.
On thinking about it more I like using a {:checked} attribute. I think that terminology fits in well with the documentation for the related --test-assumptions option (in fact I even wonder if the option should be check-assumptions to avoid implying it's strongly coupled to dafny test.
We could think of expect P; as a short form for assume {:checked} P; (that's actually allowed when compiling).
Interested in @atomb's option here too.
There was a problem hiding this comment.
What about {:check} to match assert, assume, expect as active present tense verbs.
There was a problem hiding this comment.
Another thought: perhaps it would be better if expect itself behaved this way. That is, if it had to be both verified and checked at runtime. We could change this for Dafny 4.0.
I submit that even when writing a {:test} in Dafny, you almost always believe the expression you're expect-ing to be true. Tests often look a lot like examples, and examples in Dafny should verify as well, i.e. if you can't satisfy the precondition of the function you're trying to call, it's often an indication the specified interface of the code you're testing is wrong or too weak/strong.
We would also allow expect {:axiom} P; just like assert {:axiom} P;, for easy backwards compatibility and those times it's too much work to prove P. :- expect {:axiom} ... as well.
There was a problem hiding this comment.
@seebees I'm curious whether what I'm saying above jives with your more substantial experience than mine in using expect in Dafny tests.
There was a problem hiding this comment.
For the set of contracts currently supported, --check-assumptions would be a nice improvement on naming. However, I worry it might be confusing if we extend it to evaluate other contracts at runtime, including those that, at least in principle, might be verified. What do others think?
There was a problem hiding this comment.
Note there is deeper discussion happening on the issue now, so we should move further replies there: #3410 (comment)
| @@ -3057,16 +3057,27 @@ public class CheckHasNoAssumes_Visitor : BottomUpVisitor { | |||
| // to make it more target-language idiomatic and improve performance | |||
| TrStmtList(s.ResolvedStatements, wr); | |||
|
|
|||
| } else if (stmt is ExpectStmt) { | |||
| var s = (ExpectStmt)stmt; | |||
| } else if (stmt is ExpectStmt || (stmt is AssertStmt && Attributes.Contains(stmt.Attributes, "expect"))) { | |||
There was a problem hiding this comment.
Just an observation: this also could have been written as a Rewriter that literally replaces assert {:expect} P with assert P; expect P;. The only possible tricky part is ensuring error messages still refer to the original tokens etc. but that doesn't seem too hard.
Not asking for a rewrite (especially since this one is pretty easy to do inline), but do want to make sure we identify things that create friction when pushing compilation towards more independent passes.
There was a problem hiding this comment.
That is a good idea - and I thought about it, but I'm not as familiar with rewriters. Welcome Rustans' opinion here. The current implementation does have a problem with resolution of the default message that I had to work around. A Rewriter seems conceptually cleaner.
There was a problem hiding this comment.
More thought: To add in an expect statement, one would have to make a clone of the whole AST I think (correction, one can replace the list elements of a block statement that the assert statement is in).
Also it would alter the AST, which is a problem for the formatter.
And we don't solve the problem of resolving the generated expression that is the default message.
So I'm not sure this is any cleaner.
There was a problem hiding this comment.
That's just fine and this isn't blocking: I don't actually think it's worth the effort to rewrite this, now that it's implemented and working. But I'm glad I asked because at least we're identifying what speed bumps make it harder to write features as passes.
I've been considering proposing a macro system for Dafny and this seems like a decent use case. :)
There was a problem hiding this comment.
Regarding the question of whether or not to use a rewriter. It's been my repeated experience that rewriters look appealing at first, but then they cause problems with later passes (including resolution) want to have the original form. For the situation at hand, I suggest not doing a rewrite and instead marking up the AST node (with the attribute, as would naturally happen from parsing, or using a boolean field, if the source-code mechanism were not an attribute).
There was a problem hiding this comment.
It seems like this feature would be perfect for a post-resolution rewrite. The "assert with {{:expect}} statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)" message would be produced during the rewrite, not after, so there is no issue with producing error messages for an already transformed AST.
If we allowed rewrites that happen right before compilation, so after verification, we could even replace assert {:expect} E with expect E instead of assert E; expect E, so E is not copied.
Co-authored-by: Robin Salkeld <[email protected]>
…dafny into cok-3410-assert-expect
|
Abandoning this PR |
Fixes #3410
Permits an assert statement to take a {:expect} attribute, which then makes the statement be an expect statement when compiled. It is an error if the statement is ghost and has {:expect}
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.