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.
| - 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.
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.
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?
|
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.