-
Notifications
You must be signed in to change notification settings - Fork 260
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
fix: assertion may not hold #1862
Conversation
RELEASE_NOTES.md
Outdated
@@ -3,7 +3,7 @@ | |||
- feat: `continue` statements. Like Dafny's `break` statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section [19.2](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-break-continue) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1839) | |||
- feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option `/functionSyntax` (see `/help`) allows early adoption of the new syntax. (https://github.com/dafny-lang/dafny/pull/1832) | |||
- fix: No warning "File contains no code" if a file only contains a submodule (https://github.com/dafny-lang/dafny/pull/1840) | |||
|
|||
- fix: "assertion might not hold" instead of "assertion violation" (https://github.com/dafny-lang/dafny/pull/1862) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- fix: "assertion might not hold" instead of "assertion violation" (https://github.com/dafny-lang/dafny/pull/1862) | |
- fix: "assertion might not hold" instead of "assertion violation" (https://github.com/dafny-lang/dafny/pull/1862) | |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we should try to make these release notes self-contained sentences. (And I think this is an enhancement; are calling these "fixes"?)
Something like fix: Report unprovable assertions as "assertion might not hold" instead of "assertion violation".
Also, we can write #1862 instead of the full URL.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added @fabiomadge 's suggested newline.
I reworded it like The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion.
, is that ok?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
I expect this will cause limited breakage, but it should still be listed as a breaking change if anyone has failing proofs checked in somewhere. |
Where would it be best listed as a potential breaking change? On the next release? |
We had a section for breaking changes in 3.4.0’s release notes. |
Thinking back on it, I don't think we need to list this as a breaking change. The error messages are not part of our stable interface. |
The wording "assertion violation" is misleading because we all know that many times it means that the verifier could not prove it. It caused new users to be frustrated heavily because they were looking for a counter-example, when actually the verifier was just not informed enough.
Moreover, Dafny is a verification-ready programming language, where the focus is to prove that the program is correct.
In other programming paradigms, such as bounded model checking, the focus is to prove the absence of bugs in a finite domain. This is something that could cause an "assertion violation", but here the counter-examples we have could only be approximations.
In this PR, I changed all "assertion violation" into "assertion might not hold", which is aligned with "this precondition might not hold" and all the other assertions. Other alternatives could have been
but I prefer "might not hold"
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.