Fix: Wording of assertion failure closer to semantics

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -279,7 +279,7 @@ customErrMsg is null
       : $"error is impossible: {customErrMsg}";
 
   public override string FailureDescription =>
-    customErrMsg ?? "Could not prove function precondition";
+    customErrMsg ?? "could not prove function precondition";
 
   public override string ShortDescription => "precondition";
 
@@ -297,7 +297,7 @@ customErrMsg is null
       : $"error is impossible: {customErrMsg}";
 
   public override string FailureDescription =>
-    customErrMsg ?? "Could not prove assertion";
+    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 =>
-    "could not prove that the calculation step between the previous line and this line 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 could not be proven.");
+      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 could not be proven.");
+      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:**](???) Could not prove this postcondition 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:**](???) Could not prove a postcondition on this return path.  
+        @"[**Error:**](???) could not prove a postcondition on this return path.  
 This is assertion #1 of 4 in method Abs  
 Resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (7, 11),
-        @"[**Error:**](???) Could not prove assertion  
+        @"[**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:**](???) Could not prove assertion  
+        @"[**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:**](???) Could not prove assertion  
+        @"[**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("Could not prove this postcondition: 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("Could not prove this postcondition: 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("Could not prove assertion", 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 = "Could not prove this postcondition 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 = $"Could not prove this postcondition: {postcondition}";
+          message = $"this postcondition could not be proven: {postcondition}";
         } else if (message == "Related location") {
           var tokenUri = tokenForMessage.GetDocumentUri();
           if (tokenUri == entryDocumentUri) {

Test/allocated1/Allocated1.dfy.expect

@@ -1,99 +1,99 @@
-AllocatedCommon.dfyi(23,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(24,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(25,26): Error: Could not prove assertion
+AllocatedCommon.dfyi(23,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(24,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(25,26): Error: assertion could not be proven
 AllocatedCommon.dfyi(26,30): Error: target object might not be allocated
-AllocatedCommon.dfyi(27,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(28,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(29,55): Error: Could not prove assertion
-AllocatedCommon.dfyi(30,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(31,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(32,59): Error: Could not prove assertion
-AllocatedCommon.dfyi(33,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(34,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(35,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(37,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(46,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(47,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(48,26): Error: Could not prove assertion
+AllocatedCommon.dfyi(27,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(28,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(29,55): Error: assertion could not be proven
+AllocatedCommon.dfyi(30,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(31,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(32,59): Error: assertion could not be proven
+AllocatedCommon.dfyi(33,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(34,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(35,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(37,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(46,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(47,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(48,26): Error: assertion could not be proven
 AllocatedCommon.dfyi(49,30): Error: target object might not be allocated
-AllocatedCommon.dfyi(50,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(51,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(52,55): Error: Could not prove assertion
-AllocatedCommon.dfyi(53,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(54,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(55,59): Error: Could not prove assertion
-AllocatedCommon.dfyi(56,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(57,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(58,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(60,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(82,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(83,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(84,26): Error: Could not prove assertion
+AllocatedCommon.dfyi(50,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(51,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(52,55): Error: assertion could not be proven
+AllocatedCommon.dfyi(53,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(54,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(55,59): Error: assertion could not be proven
+AllocatedCommon.dfyi(56,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(57,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(58,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(60,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(82,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(83,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(84,26): Error: assertion could not be proven
 AllocatedCommon.dfyi(85,30): Error: target object might not be allocated
-AllocatedCommon.dfyi(86,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(87,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(88,55): Error: Could not prove assertion
-AllocatedCommon.dfyi(89,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(90,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(91,59): Error: Could not prove assertion
-AllocatedCommon.dfyi(92,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(93,44): Error: Could not prove assertion
-AllocatedCommon.dfyi(94,35): Error: Could not prove assertion
-AllocatedCommon.dfyi(95,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(96,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(97,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(98,19): Error: Could not prove assertion
-AllocatedCommon.dfyi(99,19): Error: Could not prove assertion
-AllocatedCommon.dfyi(100,23): Error: Could not prove assertion
-AllocatedCommon.dfyi(118,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(119,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(120,26): Error: Could not prove assertion
+AllocatedCommon.dfyi(86,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(87,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(88,55): Error: assertion could not be proven
+AllocatedCommon.dfyi(89,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(90,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(91,59): Error: assertion could not be proven
+AllocatedCommon.dfyi(92,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(93,44): Error: assertion could not be proven
+AllocatedCommon.dfyi(94,35): Error: assertion could not be proven
+AllocatedCommon.dfyi(95,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(96,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(97,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(98,19): Error: assertion could not be proven
+AllocatedCommon.dfyi(99,19): Error: assertion could not be proven
+AllocatedCommon.dfyi(100,23): Error: assertion could not be proven
+AllocatedCommon.dfyi(118,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(119,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(120,26): Error: assertion could not be proven
 AllocatedCommon.dfyi(121,30): Error: target object might not be allocated
-AllocatedCommon.dfyi(122,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(123,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(124,55): Error: Could not prove assertion
-AllocatedCommon.dfyi(125,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(126,53): Error: Could not prove assertion
-AllocatedCommon.dfyi(127,59): Error: Could not prove assertion
-AllocatedCommon.dfyi(128,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(129,44): Error: Could not prove assertion
-AllocatedCommon.dfyi(130,35): Error: Could not prove assertion
-AllocatedCommon.dfyi(131,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(132,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(133,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(134,19): Error: Could not prove assertion
-AllocatedCommon.dfyi(135,19): Error: Could not prove assertion
-AllocatedCommon.dfyi(136,23): Error: Could not prove assertion
-AllocatedCommon.dfyi(179,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(180,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(181,26): Error: Could not prove assertion
+AllocatedCommon.dfyi(122,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(123,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(124,55): Error: assertion could not be proven
+AllocatedCommon.dfyi(125,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(126,53): Error: assertion could not be proven
+AllocatedCommon.dfyi(127,59): Error: assertion could not be proven
+AllocatedCommon.dfyi(128,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(129,44): Error: assertion could not be proven
+AllocatedCommon.dfyi(130,35): Error: assertion could not be proven
+AllocatedCommon.dfyi(131,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(132,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(133,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(134,19): Error: assertion could not be proven
+AllocatedCommon.dfyi(135,19): Error: assertion could not be proven
+AllocatedCommon.dfyi(136,23): Error: assertion could not be proven
+AllocatedCommon.dfyi(179,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(180,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(181,26): Error: assertion could not be proven
 AllocatedCommon.dfyi(182,31): Error: target object might not be allocated
-AllocatedCommon.dfyi(183,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(184,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(185,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(186,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(187,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(188,60): Error: Could not prove assertion
-AllocatedCommon.dfyi(189,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(190,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(191,44): Error: Could not prove assertion
-AllocatedCommon.dfyi(192,45): Error: Could not prove assertion
-AllocatedCommon.dfyi(193,41): Error: Could not prove assertion
-AllocatedCommon.dfyi(194,37): Error: Could not prove assertion
-AllocatedCommon.dfyi(195,57): Error: Could not prove assertion
-AllocatedCommon.dfyi(196,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(197,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(198,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(199,20): Error: Could not prove assertion
-AllocatedCommon.dfyi(200,9): Error: Could not prove assertion
-AllocatedCommon.dfyi(201,24): Error: Could not prove assertion
-AllocatedCommon.dfyi(202,27): Error: Could not prove assertion
+AllocatedCommon.dfyi(183,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(184,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(185,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(186,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(187,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(188,60): Error: assertion could not be proven
+AllocatedCommon.dfyi(189,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(190,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(191,44): Error: assertion could not be proven
+AllocatedCommon.dfyi(192,45): Error: assertion could not be proven
+AllocatedCommon.dfyi(193,41): Error: assertion could not be proven
+AllocatedCommon.dfyi(194,37): Error: assertion could not be proven
+AllocatedCommon.dfyi(195,57): Error: assertion could not be proven
+AllocatedCommon.dfyi(196,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(197,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(198,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(199,20): Error: assertion could not be proven
+AllocatedCommon.dfyi(200,9): Error: assertion could not be proven
+AllocatedCommon.dfyi(201,24): Error: assertion could not be proven
+AllocatedCommon.dfyi(202,27): Error: assertion could not be proven
 AllocatedCommon.dfyi(218,5): Error: insufficient reads clause to read field
 AllocatedCommon.dfyi(225,5): Error: insufficient reads clause to read field
-AllocatedCommon.dfyi(284,9): Error: Could not prove function precondition
-AllocatedCommon.dfyi(284,15): Error: Could not prove assertion
-AllocatedCommon.dfyi(301,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(302,26): Error: Could not prove assertion
-AllocatedCommon.dfyi(310,9): Error: Could not prove assertion
+AllocatedCommon.dfyi(284,9): Error: could not prove function precondition
+AllocatedCommon.dfyi(284,15): Error: assertion could not be proven
+AllocatedCommon.dfyi(301,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(302,26): Error: assertion could not be proven
+AllocatedCommon.dfyi(310,9): Error: assertion could not be proven
 
 Dafny program verifier finished with 15 verified, 97 errors