-
Notifications
You must be signed in to change notification settings - Fork 256
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
Combined expect/assert #3410
Comments
This would be a nice stepping stone toward having |
Question: if the expression in |
In the existing implementation of |
I'd say I'd initially tried to implement this in user code as a testing utility: method AssertAndExpect(p: bool) requires p {
expect p;
} The only issue is that then when the expect fails the error message is attached to the same source line in that method, not the caller. We could consider somehow giving user code the power to fix that. |
I'm not so fond of this suggestion. When, many moons ago, we were in discussion of what today is I see the proposal here more as a variation of An important consideration is how to explain a statement like this to a user. I think considerable confusion would arise from trying to explain
This would seem to imply that the verifier's proofs are not to be trusted. More plausible would be to give an explanation like
(It took my some effort to write that paragraph, and it still isn't great.) If we're going to prove this functionality in the language (rather than just having a
|
Thanks @RustanLeino, I agree with all of this. In particular I recall thinking of "expect" and everything suddenly clicked. :) I suggested in #3458 that we could change the semantics of How does that idea sit with you? The more I write tests in Dafny, the more I find that every Here's a very rough attempt at the explanation for users:
Note this forces us to address the awkward question of why you need to write tests even when your code is proven correct, but I think that's a good thing to build trust in the entire platform. |
There is another use case -- actually my most common one. When developing code, not everything proves and not everything executes correctly. I find it helpful when an assert does not prove to put in an expect and run the code to see if the expect obviously fails (in which case it is not just that Z3 is having a hard time). Plus if I were responsible for high-confidence code, I would want both static proof and dynamic test. |
You can always run turn off verification right? Maybe |
We plan to have What's the use-case for asserting and expecting at the same time? Wouldn't you want to expect exactly your axioms, at which point there is nothing to assert? |
Closing this issue as it has mixed support. |
Summary
Allow an attribute to combine assert and expect statements with the same predicate.
Background and Motivation
One use case for expect statements is to insert a run-time check of assertions, using this code pattern
The assertion is verified by the prover but aslo, especially during development when one is debugging assertions, the
expect is checked at runtime.
It would be convenient to allow either
assert {:expect} P;
or
expect {:assert} P;
(preferably the former),
to be interpreted as the pair of expressions alone. This also avoids the easy mistake of putting the expect before the assert.
Proposed Feature
Interpret
assert {:expect} P;
to mean
assert P;
expect P;
Alternatives
Current behavior.
The text was updated successfully, but these errors were encountered: