Revert "Change deprecated “forall ensures” to “assert by”"

This reverts commit ce5c491.
dafny-lang · Jan 3, 2024 · a2aac6d · a2aac6d
1 parent ce5c491
commit a2aac6d
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 24 deletions.
diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -91,9 +91,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    assert 0 == n * zp + ((x + n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -105,9 +103,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    assert 0 == n * zm + ((x - n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }
@@ -119,9 +115,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    assert 0 == n * zp + ((x + n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -133,9 +127,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    assert 0 == n * zm + ((x - n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }

diff --git a/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy b/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -91,9 +91,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    assert 0 == n * zp + ((x + n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -105,9 +103,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    assert 0 == n * zm + ((x - n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }
@@ -119,9 +115,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    assert 0 == n * zp + ((x + n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -133,9 +127,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    assert 0 == n * zm + ((x - n) % n) - (x % n) by {
-      LemmaMulAuto();
-    }
+    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }