Fix: Wording of assertion failure closer to semantics #3324

MikaelMayer · 2023-01-04T22:13:44Z

This PR fixes #3216 by standardizing Dafny's error messages to use "could not be proved" instead of "might not hold".

Motivation

The current "might not hold" wording has several issues:

Places doubt on the programmer rather than acknowledging Dafny's limitations
Causes user frustration when assertions are actually valid but Dafny can't prove them
Inconsistent with existing terminology - we already use "could not prove" elsewhere
Requires explanation whereas "could not prove" is self-evident

The new wording shifts focus from uncertainty about assertions to Dafny's inability to prove them, emphasizing the need to help Dafny with additional proof hints rather than questioning the assertion's validity.

Breaking Change Notice

⚠️ This PR intentionally changes error message text and will break external tools that parse Dafny output, including:

IDEs and editors with hardcoded error message patterns
CI/CD scripts that search for specific error text
Testing frameworks that depend on exact error messages
Third-party tools that analyze Dafny verification results

We consider this breaking change necessary and acceptable because:

Significantly improves user experience - reduces frustration with Dafny
More accurately reflects Dafny's semantics - focuses on proof limitations rather than assertion validity
Aligns with Dafny's user-friendly goals - makes error messages less discouraging
Provides long-term benefit - better terminology for all future users

External tool maintainers should update their parsing patterns accordingly. See docs/dev/news/3216.fix for release note details.

Error Message Changes

Core Pattern: "might not hold" → "could not be proved"

BEFORE: assertion might not hold
AFTER:  assertion could not be proved

BEFORE: This postcondition might not hold on a return path
AFTER:  this postcondition could not be proved on a return path

BEFORE: This loop invariant might not hold on entry  
AFTER:  this loop invariant could not be proved on entry

BEFORE: A precondition for this call might not hold
AFTER:  a precondition for this call could not be proved

BEFORE: function precondition might not hold
AFTER:  function precondition could not be proved

Terminology Standardization: "proven" → "proved"

BEFORE: this precondition could not be proven
AFTER:  this precondition could not be proved

Additional Patterns Standardized

BEFORE: might not be equivalent
AFTER:  could not be proved to be equivalent

BEFORE: might be null
AFTER:  could not be proved to be non-null

BEFORE: might be negative  
AFTER:  could not be proved to be non-negative

BEFORE: might refer to the same location
AFTER:  might refer to the same location (clearer positive framing)

BEFORE: might be bigger than every natural number
AFTER:  could not be proved to be a natural number

Double Negative Elimination

BEFORE: could not be proved to not underflow
AFTER:  could not be proved to remain above limit ordinal

BEFORE: could not be proved to not overflow  
AFTER:  could not be proved to remain below maximum

BEFORE: could not be proved to not be too large
AFTER:  could not be proved to be sufficiently small

Capitalization and Punctuation Consistency

BEFORE: This assertion holds.
AFTER:  this assertion holds

BEFORE: All preconditions hold for this call.
AFTER:  all preconditions hold for this call

Expected Outcome

More user-friendly error messages that focus on Dafny's limitations rather than questioning user code
Consistent terminology throughout the codebase
Improved readability through elimination of double negatives
No functional changes to verification behavior

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

This PR fixes #3216 It completely replaces the wording ".... might not hold" by "could not prove..."

…ang/dafny into fix-3216-could-not-prove

atomb · 2023-01-04T22:19:25Z

Source/DafnyCore/Verifier/ProofObligationDescription.cs


  public override string FailureDescription =>
-    customErrMsg ?? "assertion might not hold";
+    customErrMsg ?? "Could not prove assertion";


Suggested change

customErrMsg ?? "Could not prove assertion";

customErrMsg ?? "could not prove assertion";

The convention in the rest of the messages is for them to start with a lower-case letter.

atomb · 2023-01-04T22:19:47Z

Source/DafnyCore/Verifier/ProofObligationDescription.cs


  public override string FailureDescription =>
-    customErrMsg ?? "function precondition might not hold";
+    customErrMsg ?? "Could not prove function precondition";


Suggested change

customErrMsg ?? "Could not prove function precondition";

customErrMsg ?? "could not prove function precondition";

The convention in the rest of the messages is for them to start with a lower-case letter.

atomb · 2023-01-04T22:20:53Z

docs/DafnyRef/UserGuide.md

 ### 25.6.1. Verification debugging when verification fails {#sec-verification-debugging}

-Let's assume one assertion is failing ("assertion might not hold" or "postcondition might not hold"). What should you do next?
+Let's assume one assertion is failing ("Could not prove assertion" or "Could not prove postcondition"). What should you do next?


Same case distinction here.

atomb · 2023-01-04T22:21:23Z

docs/HowToFAQ/ERROR_SeqComp.md

@@ -1,5 +1,5 @@
 ---
-title: "Error: function precondition might not hold"
+title: "Error: Cannot prove function precondition"


atomb · 2023-01-04T22:21:33Z

docs/HowToFAQ/onepage.md

 Type parameter characteristics are discussed in [the reference manual](../DafnyRef/DafnyRef.html#sec-type-parameter-variance)

-# "Error: function precondition might not hold"
+# "Error: Cannot prove function precondition"


davidcok · 2023-01-04T22:52:44Z

Source/DafnyCore/Verifier/Translator.cs


      Bpl.Ensures ens = new Bpl.Ensures(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      ens.Description = new PODesc.AssertStatement(errorMessage ?? "This is the postcondition that could not be proven.");
+      ens.Description = new PODesc.AssertStatement(errorMessage ?? "this is the postcondition that could not be proven.");


If you are going with the lower case style, then remove the ending periods as well

It is usually in a full sentence, though, of the form "Error: here is something in lowercase."

Yes, but the style in dafny elsewhere is predominantly to start with lower-case and not have a period, except when there are clearly multiple sentences. I'm not wedded to this style, and am open to a team discussion, but I'd like it to be consistent.

Ah, good point. I'm fine with leaving out the periods.

atomb

Looks good!

This PR is the companion of dafny-lang/dafny#3324 We established numerous times this year that the wording "might not hold" still incorrectly provides the feeling that the postcondition is incorrect. Rather than focusing on whether assertions hold or not, this PR fixes the status by focusing on the fact that the verifier was not able to prove the assertion.

MikaelMayer · 2023-01-06T22:03:19Z

Requires
boogie-org/boogie#676
to be merged

* Fix: Error wording closer to semantics This PR is the companion of dafny-lang/dafny#3324 We established numerous times this year that the wording "might not hold" still incorrectly provides the feeling that the postcondition is incorrect. Rather than focusing on whether assertions hold or not, this PR fixes the status by focusing on the fact that the verifier was not able to prove the assertion. * Fixed tests * proven => proved. Fixed tests * Fixed one more en->ed * Fixed a test * Fixed all the boogie files with messages inline * Fixed 3 more tests * Fixed last 2 CI errors * Support for the last two CI tests * Wording for invariants as well

- Added the trace of proof even in successes - Replaced intermediate "Could not prove" and "Did prove" by "Inside " to indicate this is just a trace - Use backticks to indicate quoted code - Better error message instead of "error is impossible: This is the precondition that might not hold" - First-class support of {:error} in hover messages.

…obligation descriptions.

# Conflicts: # Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

…t text Fixed CI tests

Found and fixed missed instances of 'proven' that should be 'proved' for consistency with Boogie terminology: - QuantificationNewSyntax.dfy: function precondition comment - revealFunctions.dfy: ensures clause comment - Updated both source and bin directory versions This completes the terminology standardization effort.

Updated documentation to use 'proved' instead of 'proven' to match the standardized terminology used throughout the codebase and align with Boogie's terminology.

The error message standardization is a breaking change that may affect external tools parsing Dafny output. Updated the news entry to clearly communicate this to users and tool maintainers.

- Fix capitalization: 'dafny' → 'Dafny' in UserGuide.md - Update ERROR_SeqComp documentation to use consistent 'proved' terminology - Restore accidentally modified symlinks to their original state - Ensure documentation titles match actual error message content These changes address out-of-scope modifications and terminology inconsistencies flagged by the automated review process.

Empty log files should not be committed to version control as they serve no purpose and clutter the repository. This file was accidentally included and is unrelated to the error message standardization effort.

- Replace confusing double-negative logic with clearer positive framing - Improve grammatical structure for better readability - Maintain consistency with PR's standardization goals

- Keep original error message wording that Dafny actually produces - Use proper Dafny terminology (fields, not elements)

- Update error message expectations to use 'could not be proved' wording - Fix documentation typo: 'proven' -> 'proved' - Align with PR #3324 error message standardization

atomb

Your review.sh script from #6318 was very helpful!

It pointed out one inconsistency in the error messages, exhibited by modified.dfy, which I commented on below.

It also pointed out some slightly out-of-scope changes related to command-line handling in docs/DafnyRef/UserGuide.md, but I think they all seem reasonable and I don't object to including them.

atomb · 2025-08-21T01:28:59Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/modifiable.dfy.expect

+modifiable.dfy(42,6): Error: modified field could not be proved to be in the current modifies clause
 Asserted expression: c == s[1]
-modifiable.dfy(50,5): Error: assignment might update an array element not in the enclosing context's modifies clause
+modifiable.dfy(50,5): Error: modified field could not be proved to be in the current modifies clause


The new message talks about a field, but the location being updated is an array element, as the old description correctly stated.

- Change 'modified field' to use the actual description ('an object' vs 'an array element') - Update modifiable.dfy.expect to reflect correct error messages - Addresses review comment about incorrect 'field' terminology for array elements

- Field assignments: 'modified field could not be proved...' - Array assignments: 'modified array location could not be proved...' - Fixed at construction sites to avoid switch statement repetition - Updated modifiable.dfy.expect accordingly

- Array assignments now show 'modified array location' - Field assignments continue to show 'modified field' - Updated Array.dfy.expect, LoopModifies.dfy.expect, TraitUsingParentMembers.dfy.expect

- Array assignment a[1] := 3 should show 'modified array location'

- Field assignments in forall: 'field' -> 'modified field could not be proved...' - Array assignments in forall: 'array location' -> 'modified array location could not be proved...' - This fixes the remaining CI failures in integration test partitions 1 and 3

- Trigger CI to test final fixes - 18/20 tests now passing (90% success rate) - Only integration-tests partition 3 still failing

- This file doesn't belong in the repository

- Line 332 is 'x :| assume x == 10;' where x is a class field - Should be 'modified field' not 'modified array location' - This fixes the last failing integration test

Currently, reviewing long PRs, like PRs that changes multiple expect files, is discouraging. This PR automates the reviewing process by delegating some portion of reviewing, i.e. low-level reviewing, to an agent such as Amazon Q or Claude Code ### What was changed? I added a script `./review.sh` that requires a PR number and automatically performs a review of every change to see if they conform to the PR description. It clones the repository, lists all the files, and input maximum 500 lines of diff into a prompt that asks if the diff is consistent with what we could have expected from the PR description. Sample output while the script is running live. ``` ========================================= Current review concerns: (No issues found so far) Progress: 21/346 files reviewed so far Currently reviewing: docs/DafnyRef/UserGuide.5.expect ========================================= ``` ### How has this been tested? #### Exiting PR I ran this script on #3324 to ensure the PR description is consistent with the changes. It already detected the following issues: - The PR description omitted to mention that the error messages could break integration with tools depending on the error messages - Two files were added that shouldn't have been committed - One document line was not up to date. - Capitalization of Dafny was inconsistent in the doc. #### Self-test: Positive case I also tested this script on this PR itself. Here was the output: ``` ======================================== Current review concerns: (No issues found so far) Progress: 0/1 files reviewed so far Currently reviewing: Scripts/review.sh ========================================= ``` ``` ========================================= 📊 FINAL CODE REVIEW SUMMARY ========================================= Files processed: 1 Files analyzed: 1 Files skipped: 0 Files passed: 1 Files failed: 0 ✅ All analyzed files passed code review! ✅ PR #6318 looks good to merge 🎉 Code review complete! ``` #### Self-test: Negative case: When deleting a line in the Makefile, we immediately get meaningful feedback ``` ========================================= Current review concerns: Makefile: Makefile: DIR variable removed but still referenced in test-dafny and tests-verbose targets, causing undefined variable errors Progress: 1/2 files reviewed so far Currently reviewing: Scripts/review.sh ========================================= ``` and then when the analysis is finished, we see ``` ========================================= 📊 FINAL CODE REVIEW SUMMARY ========================================= Files processed: 2 Files analyzed: 2 Files skipped: 0 Files passed: 1 Files failed: 1 ❌ Issues found in 1 file(s): Makefile: Makefile: DIR variable removed but still referenced in test-dafny and tests-verbose targets, causing undefined variable errors 🧹 Cleaning up successful review files... 💡 Review output files for failed files are available in the current directory ❌ Consider addressing these concerns before merging 🎉 Code review complete! ⚠️ IMPORTANT: This AI review is a tool to assist human reviewers. You are ultimately responsible for the actual quality of the review. Just because the AI doesn't flag anything doesn't mean the PR is actually free of issues. Always apply your own judgment and expertise. ``` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Fix: Wording of assertion failure to match what happens

8e7320a

This PR fixes #3216 It completely replaces the wording ".... might not hold" by "could not prove..."

MikaelMayer requested a review from atomb January 4, 2023 22:13

MikaelMayer and others added 3 commits January 4, 2023 16:14

Merge branch 'master' into fix-3216-could-not-prove

7acc626

Fixed case for "Could not"

3a1231e

Merge branch 'fix-3216-could-not-prove' of https://github.com/dafny-l…

edaefcc

…ang/dafny into fix-3216-could-not-prove

atomb requested changes Jan 4, 2023

View reviewed changes

MikaelMayer added 2 commits January 4, 2023 16:34

Lowercase

174e304

Passive voice so that important stuff is at the beginning

4350bcd

davidcok previously requested changes Jan 4, 2023

View reviewed changes

MikaelMayer and others added 3 commits January 5, 2023 10:22

Review comments

83395c3

Review comments

ec1d2e6

Merge branch 'master' into fix-3216-could-not-prove

a237a0e

MikaelMayer requested review from atomb and davidcok January 5, 2023 16:25

atomb previously approved these changes Jan 6, 2023

View reviewed changes

MikaelMayer mentioned this pull request Jan 6, 2023

Fix: Error wording closer to semantics boogie-org/boogie#676

Merged

MikaelMayer and others added 11 commits March 3, 2023 15:02

Support for {:error} on hover also on postconditions

c3c5516

Review comments

32cb31d

Review comments: Got rid of patches by integrating better with Proof …

05227f6

…obligation descriptions.

Merge branch 'master' into feat-better-error-messages

60ec8d9

Merge branch 'master' into feat-better-error-messages

0aac9fe

Merge branch 'master' into feat-better-error-messages

b136d48

Merge branch 'master' into feat-better-error-messages

8d2b241

# Conflicts: # Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

Fixed CI

b831daa

Ensured EnsuresDescription and PostconditionDescription share relevan…

d7a32d3

…t text Fixed CI tests

Ensure test is deterministic

be50afe

MikaelMayer mentioned this pull request Jul 29, 2025

Class/Trait Invariants #6313

Open

MikaelMayer mentioned this pull request Jul 31, 2025

Chore: Review script to review long pull requests #6318

Merged

MikaelMayer and others added 10 commits July 31, 2025 19:56

Fix UserGuide.md terminology: 'proven' → 'proved' for consistency

1d42db5

Updated documentation to use 'proved' instead of 'proven' to match the standardized terminology used throughout the codebase and align with Boogie's terminology.

Update release notes to mention breaking change for external tools

27a03a2

The error message standardization is a breaking change that may affect external tools parsing Dafny output. Updated the news entry to clearly communicate this to users and tool maintainers.

Remove empty log file ubuntu_xunit_logs.txt

9a0b2c1

Empty log files should not be committed to version control as they serve no purpose and clutter the repository. This file was accidentally included and is unrelated to the error message standardization effort.

Fix error message clarity issues

ab77899

- Replace confusing double-negative logic with clearer positive framing - Improve grammatical structure for better readability - Maintain consistency with PR's standardization goals

Revert expect files to match actual Dafny output

cb6b35c

- Keep original error message wording that Dafny actually produces - Use proper Dafny terminology (fields, not elements)

Merge branch 'master' into fix-3216-could-not-prove

8a2d1a8

Update test expectations after merge with master

f227427

- Update error message expectations to use 'could not be proved' wording - Fix documentation typo: 'proven' -> 'proved' - Align with PR #3324 error message standardization

Fix ReadsOnMethods expect file to match actual output

7e98f57

Merge branch 'master' into fix-3216-could-not-prove

a0178f2

atomb requested changes Aug 21, 2025

View reviewed changes

MikaelMayer added 2 commits August 27, 2025 21:20

atomb previously approved these changes Aug 27, 2025

View reviewed changes

MikaelMayer added 2 commits August 28, 2025 12:33

Update expect files for array vs field assignments

3bc9702

- Array assignments now show 'modified array location' - Field assignments continue to show 'modified field' - Updated Array.dfy.expect, LoopModifies.dfy.expect, TraitUsingParentMembers.dfy.expect

Merge branch 'master' into fix-3216-could-not-prove

d612fa9

MikaelMayer dismissed atomb’s stale review via d612fa9 August 28, 2025 12:33

MikaelMayer enabled auto-merge (squash) August 28, 2025 12:36

MikaelMayer added 5 commits August 28, 2025 13:05

Fix memorylocations-errors.dfy.expect for array assignment

2a65a89

- Array assignment a[1] := 3 should show 'modified array location'

Add PR description

3f427db

- Trigger CI to test final fixes - 18/20 tests now passing (90% success rate) - Only integration-tests partition 3 still failing

Remove PR_DESCRIPTION.md

689649d

- This file doesn't belong in the repository

Fix Array.dfy.expect line 332 - field assignment not array

ae0806e

- Line 332 is 'x :| assume x == 10;' where x is a class field - Should be 'modified field' not 'modified array location' - This fixes the last failing integration test

atomb approved these changes Aug 28, 2025

View reviewed changes

MikaelMayer merged commit 660219c into master Aug 28, 2025
21 checks passed

MikaelMayer deleted the fix-3216-could-not-prove branch August 28, 2025 20:28

	customErrMsg ?? "Could not prove assertion";
	customErrMsg ?? "could not prove assertion";

	customErrMsg ?? "Could not prove function precondition";
	customErrMsg ?? "could not prove function precondition";

Fix: Wording of assertion failure closer to semantics #3324

Fix: Wording of assertion failure closer to semantics #3324

Uh oh!

Conversation

MikaelMayer commented Jan 4, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation

Breaking Change Notice

Error Message Changes

Core Pattern: "might not hold" → "could not be proved"

Terminology Standardization: "proven" → "proved"

Additional Patterns Standardized

Double Negative Elimination

Capitalization and Punctuation Consistency

Expected Outcome

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

atomb left a comment

Choose a reason for hiding this comment

Uh oh!

MikaelMayer commented Jan 6, 2023

Uh oh!

atomb left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

MikaelMayer commented Jan 4, 2023 •

edited

Loading