Fix: Wording of assertion failure closer to semantics

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -11,7 +11,7 @@ public abstract class ProofObligationDescription : Boogie.ProofObligationDescrip
 
 public class DivisorNonZero : ProofObligationDescription {
   public override string SuccessDescription =>
-    "divisor is always non-zero.";
+    "divisor is always non-zero";
 
   public override string FailureDescription =>
     "possible division by zero";
@@ -279,7 +279,7 @@ customErrMsg is null
       : $"error is impossible: {customErrMsg}";
 
   public override string FailureDescription =>
-    customErrMsg ?? "function precondition might not hold";
+    customErrMsg ?? "function precondition could not be proven";
 
   public override string ShortDescription => "precondition";
 
@@ -297,7 +297,7 @@ customErrMsg is null
       : $"error is impossible: {customErrMsg}";
 
   public override string FailureDescription =>
-    customErrMsg ?? "assertion might not hold";
+    customErrMsg ?? "assertion could not be proven";
 
   public override string ShortDescription => "assert statement";
 
@@ -331,7 +331,7 @@ public class CalculationStep : ProofObligationDescription {
     "the calculation step between the previous line and this line always holds";
 
   public override string FailureDescription =>
-    "the calculation step between the previous line and this line might not hold";
+    "the calculation step between the previous line and this line could not be proven";
 
   public override string ShortDescription => "calc step";
 }

Source/DafnyCore/Verifier/Translator.cs

@@ -7233,7 +7233,7 @@ Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessa
       Contract.Ensures(Contract.Result<Bpl.Ensures>() != null);
 
       Bpl.Ensures ens = new Bpl.Ensures(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      ens.Description = new PODesc.AssertStatement(errorMessage ?? "This is the postcondition that might not hold.");
+      ens.Description = new PODesc.AssertStatement(errorMessage ?? "this is the postcondition that could not be proven.");
       return ens;
     }
 
@@ -7242,7 +7242,7 @@ Bpl.Requires Requires(IToken tok, bool free, Bpl.Expr condition, string errorMes
       Contract.Requires(condition != null);
       Contract.Ensures(Contract.Result<Bpl.Requires>() != null);
       Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      req.Description = new PODesc.AssertStatement(errorMessage ?? "This is the precondition that might not hold.");
+      req.Description = new PODesc.AssertStatement(errorMessage ?? "this is the precondition that could not be proven");
       return req;
     }
 

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -48,20 +48,20 @@ method Abs(x: int) returns (y: int)
 ", "testFile.dfy");
       // When hovering the postcondition, it should display the position of the failing path
       await AssertHoverMatches(documentItem, (2, 15),
-        @"[**Error:**](???) This postcondition might not hold on a return path.  
+        @"[**Error:**](???) this postcondition could not be proven on a return path  
 This is assertion #1 of 4 in method Abs  
 Resource usage: ??? RU  
 Return path: testFile.dfy(6, 5)"
       );
       // When hovering the failing path, it does not display the position of the failing postcondition
       // because the IDE extension already does it.
       await AssertHoverMatches(documentItem, (5, 4),
-        @"[**Error:**](???) A postcondition might not hold on this return path.  
+        @"[**Error:**](???) a postcondition could not be proven on this return path  
 This is assertion #1 of 4 in method Abs  
 Resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (7, 11),
-        @"[**Error:**](???) assertion might not hold  
+        @"[**Error:**](???) assertion could not be proven  
 This is assertion #2 of 4 in method Abs  
 Resource usage: 9K RU"
       );
@@ -86,7 +86,7 @@ await SetUp(o => {
 }
 ", "testfile.dfy");
       await AssertHoverMatches(documentItem, (1, 12),
-        @"[**Error:**](???) assertion might not hold  
+        @"[**Error:**](???) assertion could not be proven  
 This is the only assertion in [batch](???) #??? of ??? in method f  
 [Batch](???) #??? resource usage: ??? RU"
       );
@@ -123,7 +123,7 @@ await AssertHoverMatches(documentItem, (2, 12),
 [Batch](???) #1 resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (3, 26),
-        @"[**Error:**](???) assertion might not hold  
+        @"[**Error:**](???) assertion could not be proven  
 This is assertion #1 of 2 in [batch](???) #2 of 2 in function f  
 [Batch](???) #2 resource usage: ??? RU"
       );

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -341,7 +341,7 @@ decreases y
       Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[1].Severity);
       Assert.AreEqual(1, diagnostics[0].RelatedInformation.Count());
       var relatedInformation = diagnostics[0].RelatedInformation.First();
-      Assert.AreEqual("This postcondition might not hold: product >= 0", relatedInformation.Message);
+      Assert.AreEqual("this postcondition could not be proven: product >= 0", relatedInformation.Message);
       Assert.AreEqual(new Range(new Position(2, 30), new Position(2, 42)), relatedInformation.Location.Range);
       await AssertNoDiagnosticsAreComing(CancellationToken);
     }
@@ -666,9 +666,9 @@ modifies this
       Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity);
       var relatedInformation = diagnostics[0].RelatedInformation.ToArray();
       Assert.AreEqual(2, relatedInformation.Length);
-      Assert.AreEqual("This postcondition might not hold: Valid()", relatedInformation[0].Message);
+      Assert.AreEqual("this postcondition could not be proven: Valid()", relatedInformation[0].Message);
       Assert.AreEqual(new Range((14, 16), (14, 23)), relatedInformation[0].Location.Range);
-      Assert.AreEqual("Could not prove: b < c", relatedInformation[1].Message);
+      Assert.AreEqual("could not prove: b < c", relatedInformation[1].Message);
       Assert.AreEqual(new Range((9, 11), (9, 16)), relatedInformation[1].Location.Range);
       await AssertNoDiagnosticsAreComing(CancellationToken);
     }

Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs

@@ -102,7 +102,7 @@ DidChangeTextDocumentParams MakeChange(int? version, Range range, string text) {
       Assert.IsNotNull(document);
       Assert.AreEqual(documentItem.Version + 11, document.Version);
       Assert.AreEqual(1, document.Diagnostics.Count());
-      Assert.AreEqual("assertion might not hold", document.Diagnostics.First().Message);
+      Assert.AreEqual("assertion could not be proven", document.Diagnostics.First().Message);
     }
 
     [TestMethod, Timeout(MaxTestExecutionTimeMs)]

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

@@ -204,7 +204,7 @@ string GetDescription(Boogie.ProofObligationDescription? description) {
             if (currentlyHoveringPostcondition &&
                   (failureDescription == new PostconditionDescription().FailureDescription ||
                    failureDescription == new EnsuresDescription().FailureDescription)) {
-              failureDescription = "This postcondition might not hold on a return path.";
+              failureDescription = "this postcondition could not be proven on a return path";
             }
             return $"{obsolescence}[**Error:**](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-debugging) " +
                    failureDescription;

Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

@@ -84,7 +84,7 @@ public void ReportBoogieError(ErrorInformation error) {
     private readonly string entryDocumentsource;
 
     public static string FormatRelated(string related) {
-      return $"Could not prove: {related}";
+      return $"could not prove: {related}";
     }
 
     private IEnumerable<DiagnosticRelatedInformation> CreateDiagnosticRelatedInformationFor(IToken token, string message) {
@@ -93,7 +93,7 @@ private IEnumerable<DiagnosticRelatedInformation> CreateDiagnosticRelatedInforma
         var rangeLength = range.EndToken.pos + range.EndToken.val.Length - range.StartToken.pos;
         if (message == PostConditionFailingMessage) {
           var postcondition = entryDocumentsource.Substring(range.StartToken.pos, rangeLength);
-          message = $"This postcondition might not hold: {postcondition}";
+          message = $"this postcondition could not be proven: {postcondition}";
         } else if (message == "Related location") {
           var tokenUri = tokenForMessage.GetDocumentUri();
           if (tokenUri == entryDocumentUri) {