Issue a warning for the almost-always-a-mistake of putting an implica…

…tion inside an existential quantifier

Source/Dafny/Resolver.cs

@@ -5427,6 +5427,17 @@ public CheckTypeInference_Visitor(Resolver resolver, ICodeContext codeContext)
             }
           }
 
+
+          if (e is ExistsExpr && e.Range == null) {
+            var binBody = ((ExistsExpr)e).Term as BinaryExpr;
+            if (binBody != null && binBody.Op == BinaryExpr.Opcode.Imp) {  // check Op, not ResolvedOp, in order to distinguish ==> and <==
+              // apply the wisdom of Claude Marche: issue a warning here
+              resolver.reporter.Warning(MessageSource.Resolver, e.tok,
+                "the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; " +
+                "if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning");
+            }
+          }
+
         } else if (expr is MemberSelectExpr) {
           var e = (MemberSelectExpr)expr;
           if (e.Member is Function || e.Member is Method) {

Test/dafny0/ComputationsNeg.dfy

@@ -2,31 +2,31 @@
 // RUN: %diff "%s.expect" "%t"
 
 function bad(n: nat): nat
-  decreases n;
+  decreases n
 {
-  bad(n+1)
+  bad(n+1)  // error: termination failure
 }
 ghost method go_bad()
-  ensures bad(0)==0;
-{
+  ensures bad(0)==0
+{  // error: postcondition violation
 }
 
 datatype Nat = Zero | Succ(tail: Nat)
 predicate ThProperty(step: nat, t: Nat, r: nat)
 {
   match t
   case Zero => true
-  case Succ(o) => step>0 && exists ro:nat, ss :: ss == step-1 ==> ThProperty(ss, o, ro) // WISH: auto-generate ss
+  case Succ(o) => step>0 && exists ro:nat, ss :: ss == step-1 && ThProperty(ss, o, ro) // WISH: auto-generate ss
 }
 ghost method test_ThProperty()
-  ensures ThProperty(10, Succ(Zero), 0);
-{
+  ensures ThProperty(10, Succ(Zero), 0)
+{  // error: postcondition violation
 //  assert ThProperty(9, Zero, 0);
 }
 
 // The following is a test that well-typedness antecednets are included in the literal axioms
 function StaticFact(n: nat): nat
-  ensures 0 < StaticFact(n);
+  ensures 0 < StaticFact(n)
 {
   if n == 0 then 1 else n * StaticFact(n - 1)
 }

Test/dafny0/ResolutionErrors.dfy

@@ -2678,3 +2678,37 @@ module RegressionTest {
     }
   }
 }
+
+module ExistsImpliesWarning {
+  method M(a: array<int>, b: array<int>)
+    requires a.Length == b.Length
+    requires exists i :: 0 <= i < a.Length ==> a[i] == b[i]  // warning
+    requires exists i :: true && (0 <= i < a.Length ==> a[i] == b[i])
+    requires exists i :: (0 <= i < a.Length ==> a[i] == b[i])
+    requires exists i | 0 <= i < a.Length :: true ==> a[i] == b[i]
+    requires exists i | 0 <= i < a.Length :: a[i] == b[i]
+    requires exists i | 0 <= i < a.Length ==> a[i] == b[i] :: true
+    requires exists i :: !(0 <= i < a.Length) || a[i] == b[i]
+    requires exists i :: a[i] == b[i] <== 0 <= i < a.Length  // warning
+    requires exists i :: !(0 <= i < a.Length && a[i] != b[i])
+    requires exists i :: 0 <= i < a.Length && a[i] == b[i]
+    requires exists i :: true ==> (0 <= i < a.Length && a[i] == b[i])  // warning
+  {
+  }
+
+  method N(a: array<int>, b: array<int>)
+    requires a.Length == b.Length
+    requires forall i :: 0 <= i < a.Length ==> a[i] == b[i]
+    requires forall i :: true && (0 <= i < a.Length ==> a[i] == b[i])
+    requires forall i :: (0 <= i < a.Length ==> a[i] == b[i])
+    requires forall i | 0 <= i < a.Length :: true ==> a[i] == b[i]
+    requires forall i | 0 <= i < a.Length :: a[i] == b[i]
+    requires forall i | 0 <= i < a.Length ==> a[i] == b[i] :: true
+    requires forall i :: !(0 <= i < a.Length) || a[i] == b[i]
+    requires forall i :: a[i] == b[i] <== 0 <= i < a.Length
+    requires forall i :: !(0 <= i < a.Length && a[i] != b[i])
+    requires forall i :: 0 <= i < a.Length && a[i] == b[i]
+    requires forall i :: true ==> (0 <= i < a.Length && a[i] == b[i])
+  {
+  }
+}

Test/dafny0/ResolutionErrors.dfy.expect

@@ -415,4 +415,6 @@ ResolutionErrors.dfy(2638,26): Error: type parameter (G) passed to method Gimmie
 ResolutionErrors.dfy(2651,50): Error: type of the receiver is not fully determined at this program point
 ResolutionErrors.dfy(2677,11): Error: name of type (Cache) is used as a variable
 ResolutionErrors.dfy(2677,17): Error: incorrect type for selection into ? (got X)
+ResolutionErrors.dfy(2685,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning
+ResolutionErrors.dfy(2695,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning
 414 resolution/type errors detected in ResolutionErrors.dfy

Test/wishlist/assign-such-that-antecedent.dfy

@@ -10,7 +10,7 @@ method M(a: int, b: int) {
 }
 
 method M_assert_exists(a: int, b: int) {
-  assert exists s :: b != 0 ==> s == a / b && Q(s);  // WISH
+  assert exists s :: (b != 0 ==> s == a / b && Q(s));  // WISH
 }
 
 method N(a: int, b: int)