-
Notifications
You must be signed in to change notification settings - Fork 261
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
Use proof dependencies for more thorough brittleness reduction warnings #5261
Comments
Nice feature Nitpick: in the user facing messages, I think we should talk about performance instead of brittleness. Addressing these warnings will improve verification performance, even if the user is not having any issues with brittleness. |
Do we know whether |
Also, suppose you have a sequence of assertions,
where each is used to prove the next one, then it seems the feature described in this issue would guide the user to write this as a nesting of by blocks
Syntactically that looks much worse. Are we missing a language construct here? |
Unfortunately, using |
Yeah, I agree. I suspect there may be a language construct that would make it nicer. I'll mull that over, but feel free to suggest something if it comes to mind! |
Currently when use you That way, if you have assert X by { Y; }
assert Z; and we translate it into this Boogie:
Then with
Note that |
Summary
Issues #5253 and issue #5259 describe features to help guide Dafny programmers toward reducing brittleness in the verification of their code. This issue describes additional features that extend that capability by building on proof dependencies.
Background and Motivation
Brittleness, where verification can alternate between success and failure after seemingly trivial changes, is a key challenge in Dafny. In general, one of the more effective techniques for reducing brittleness is to limit the information available to the solver. Proof dependency analysis can help us understand what facts are necessary for what proof goals, and therefore suggest ways to refactor the code to reduce brittleness.
Proposed Feature
Implement new warnings that identify instance of the following patterns:
assert
statements that are needed only to help discharge one assertion, and therefore could be moved into aby
block of anassert
statement (or a method call, when Addby
blocks to function and method calls #5192 is complete).Alternatives
Like #5253 and #5253, these suggestions could be static, in a document. But, like those issue, direct, active feedback, would help accelerate the process. In addition, it automates a dependency analysis process that is difficult to perform manually.
The text was updated successfully, but these errors were encountered: