Disallow parentheses-less declarations of predicates and co-predicates, along with a backward-compatibility warning message if such declarations are attempted

2 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index b6be031a..121b33aa 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -31,7 +31,7 @@ module B refines A {
       modifies this;  // error: cannot add a modifies clause
       ensures 0 <= x;  // fine
 
-    predicate abc  // error: cannot replace a field with a predicate
+    predicate abc()  // error: cannot replace a field with a predicate
     var xyz: bool;  // error: ...or even with another field
 
     function F   // error: cannot replace a "function method" with a "function"
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 6255ee96..d5a9d901 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -5,7 +5,7 @@ abstract module A {
   import L = Library;

   class {:autocontracts} StoreAndRetrieve<Thing(==)> {

     ghost var Contents: set<Thing>;

-    predicate Valid

+    predicate Valid()

     {

       true

     }

@@ -31,7 +31,7 @@ abstract module A {
 module B refines A {

   class StoreAndRetrieve<Thing(==)> {

     var arr: seq<Thing>;

-    predicate Valid

+    predicate Valid()

     {

       Contents == set x | x in arr

     }