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

10 files changed, 80 insertions, 93 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 8ec51b82..c195e14b 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -607,13 +607,13 @@ namespace Microsoft.Dafny
       }

 

       if (f is Predicate) {

-        return new Predicate(Tok(f.tok), newName, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals,

+        return new Predicate(Tok(f.tok), newName, f.IsStatic, f.IsGhost, tps, formals,

           req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null);

       } else if (f is CoPredicate) {

-        return new CoPredicate(Tok(f.tok), newName, f.IsStatic, tps, f.OpenParen, formals,

+        return new CoPredicate(Tok(f.tok), newName, f.IsStatic, tps, formals,

           req, reads, ens, body, CloneAttributes(f.Attributes), null);

       } else {

-        return new Function(Tok(f.tok), newName, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),

+        return new Function(Tok(f.tok), newName, f.IsStatic, f.IsGhost, tps, formals, CloneType(f.ResultType),

           req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);

       }

     }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2d3d93d6..25831c44 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -586,7 +586,6 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter>
      IToken/*!*/ id;

      Attributes attrs = null;

      List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

-     IToken openParen;

      List<Formal/*!*/> ins = new List<Formal/*!*/>();

      List<Formal/*!*/> outs = new List<Formal/*!*/>();

      List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

@@ -611,13 +610,13 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter>
   NoUSIdent<out id>

   (

     [ GenericParameters<typeArgs> ]

-    Formals<true, true, ins, out openParen>

+    Formals<true, true, ins>

     [ ( "yields"

       | "returns"           (. SemErr(t, "iterators don't have a 'returns' clause; did you mean 'yields'?"); .)

       )

-      Formals<false, true, outs, out openParen>

+      Formals<false, true, outs>

     ]

-  | "..."                                       (. signatureEllipsis = t; openParen = Token.NoToken; .)

+  | "..."                                       (. signatureEllipsis = t; .)

   )

   { IteratorSpec<reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs> }

   [ BlockStmt<out body, out bodyStart, out bodyEnd>

@@ -655,7 +654,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      bool hasName = false;  IToken keywordToken;

      Attributes attrs = null;

      List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

-     IToken openParen;

      List<Formal/*!*/> ins = new List<Formal/*!*/>();

      List<Formal/*!*/> outs = new List<Formal/*!*/>();

      List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();

@@ -715,11 +713,11 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   .)

   (

     [ GenericParameters<typeArgs> ]

-    Formals<true, !mmod.IsGhost, ins, out openParen>

+    Formals<true, !mmod.IsGhost, ins>

     [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)

-      Formals<false, !mmod.IsGhost, outs, out openParen>

+      Formals<false, !mmod.IsGhost, outs>

     ]

-  | "..."                                       (. signatureEllipsis = t; openParen = Token.NoToken; .)

+  | "..."                                       (. signatureEllipsis = t; .)

   )

   { MethodSpec<req, mod, ens, dec, ref decAttrs, ref modAttrs> }

   [ BlockStmt<out body, out bodyStart, out bodyEnd>

@@ -810,9 +808,9 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
   | "decreases" { IF(IsAttribute()) Attribute<ref decrAttrs> } DecreasesList<decreases, false> SYNC ";"

   )

   .

-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen.>

-= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)

-  "("                                                                  (. openParen = t; .)

+Formals<.bool incoming, bool allowGhostKeyword, List<Formal> formals.>

+= (. Contract.Requires(cce.NonNullElements(formals)); IToken id;  Type ty;  bool isGhost; .)

+  "("

   [

     GIdentType<allowGhostKeyword, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

     { "," GIdentType<allowGhostKeyword, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

@@ -943,10 +941,10 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      Expression body = null;

      bool isPredicate = false;  bool isCoPredicate = false;

      bool isFunctionMethod = false;

-     IToken openParen = null;

      IToken bodyStart = Token.NoToken;

      IToken bodyEnd = Token.NoToken;

      IToken signatureEllipsis = null;

+     bool missingOpenParen;

   .)

   /* ----- function ----- */

   ( "function"

@@ -958,11 +956,10 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
     NoUSIdent<out id>

     (

       [ GenericParameters<typeArgs> ]

-      Formals<true, isFunctionMethod, formals, out openParen>

+      Formals<true, isFunctionMethod, formals>

       ":"

       Type<out returnType>

-    | "..."                    (. signatureEllipsis = t;

-                                  openParen = Token.NoToken; .)

+    | "..."                    (. signatureEllipsis = t; .)

     )

 

   /* ----- predicate ----- */

@@ -974,13 +971,12 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
     { Attribute<ref attrs> }

     NoUSIdent<out id>

     (

-      [ GenericParameters<typeArgs> ]

-      [ Formals<true, isFunctionMethod, formals, out openParen>

-        [ ":"                  (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)

-        ]

+      [ GenericParameters<typeArgs> ]                  (. missingOpenParen = true; .)

+      [ Formals<true, isFunctionMethod, formals>       (. missingOpenParen = false; .)

+      ]                                                (. if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the predicate takes no additional arguments"); } .)

+      [ ":"                    (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)

       ]

-    | "..."                    (. signatureEllipsis = t;

-                                  openParen = Token.NoToken; .)

+    | "..."                    (. signatureEllipsis = t; .)

     )

 

   /* ----- copredicate ----- */

@@ -990,13 +986,12 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
     { Attribute<ref attrs> }

     NoUSIdent<out id>

     (

-      [ GenericParameters<typeArgs> ]

-      [ Formals<true, isFunctionMethod, formals, out openParen>

-        [ ":"                  (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)

-        ]

+      [ GenericParameters<typeArgs> ]                  (. missingOpenParen = true; .)

+      [ Formals<true, isFunctionMethod, formals>       (. missingOpenParen = false; .)

+      ]                                                (. if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less co-predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the co-predicate takes no additional arguments"); } .)

+      [ ":"                    (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)

       ]

-    | "..."                    (. signatureEllipsis = t;

-                                  openParen = Token.NoToken; .)

+    | "..."                    (. signatureEllipsis = t; .)

     )

   )

 

@@ -1010,13 +1005,13 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
 

      IToken tok = theVerifyThisFile ? id : new IncludeToken(id);

      if (isPredicate) {

-        f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

+        f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, formals,

                           reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);

      } else if (isCoPredicate) {

-        f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, openParen, formals,

+        f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, formals,

                           reqs, reads, ens, body, attrs, signatureEllipsis);

      } else {

-        f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

+        f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, formals, returnType,

                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);

      }

      f.BodyStartTok = bodyStart;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index faf79a30..598b53da 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -166,12 +166,12 @@ namespace Microsoft.Dafny {
         };

         var readsFrame = new List<FrameExpression> { new FrameExpression(tok, readsIS, null) };

         var req = new Function(tok, "requires", false, true,

-          new List<TypeParameter>(), tok, args, Type.Bool,

+          new List<TypeParameter>(), args, Type.Bool,

           new List<Expression>(), readsFrame, new List<Expression>(),

           new Specification<Expression>(new List<Expression>(), null),

           null, new Attributes("axiom", new List<Attributes.Argument>(), null), null);

         var reads = new Function(tok, "reads", false, true,

-          new List<TypeParameter>(), tok, args, new SetType(new ObjectType()),

+          new List<TypeParameter>(), args, new SetType(new ObjectType()),

           new List<Expression>(), readsFrame, new List<Expression>(),

           new Specification<Expression>(new List<Expression>(), null),

           null, new Attributes("axiom", new List<Attributes.Argument>(), null), null);

@@ -2645,7 +2645,6 @@ namespace Microsoft.Dafny {
   public class Function : MemberDecl, TypeParameter.ParentType, ICallable {

     public bool IsRecursive;  // filled in during resolution

     public readonly List<TypeParameter> TypeArgs;

-    public readonly IToken OpenParen;  // can be null (for predicates), if there are no formals

     public readonly List<Formal> Formals;

     public readonly Type ResultType;

     public readonly List<Expression> Req;

@@ -2700,7 +2699,7 @@ namespace Microsoft.Dafny {
     /// Note, functions are "ghost" by default; a non-ghost function is called a "function method".

     /// </summary>

     public Function(IToken tok, string name, bool isStatic, bool isGhost,

-                    List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,

+                    List<TypeParameter> typeArgs, List<Formal> formals, Type resultType,

                     List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                     Expression body, Attributes attributes, IToken signatureEllipsis)

       : base(tok, name, isStatic, isGhost, attributes) {

@@ -2715,7 +2714,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

       this.TypeArgs = typeArgs;

-      this.OpenParen = openParen;

       this.Formals = formals;

       this.ResultType = resultType;

       this.Req = req;

@@ -2751,10 +2749,10 @@ namespace Microsoft.Dafny {
     }

     public readonly BodyOriginKind BodyOrigin;

     public Predicate(IToken tok, string name, bool isStatic, bool isGhost,

-                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,

+                     List<TypeParameter> typeArgs, List<Formal> formals,

                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                      Expression body, BodyOriginKind bodyOrigin, Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {

+      : base(tok, name, isStatic, isGhost, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {

       Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);

       BodyOrigin = bodyOrigin;

     }

@@ -2768,10 +2766,10 @@ namespace Microsoft.Dafny {
     public readonly Formal K;

     public readonly CoPredicate Co;

     public PrefixPredicate(IToken tok, string name, bool isStatic,

-                     List<TypeParameter> typeArgs, IToken openParen, Formal k, List<Formal> formals,

+                     List<TypeParameter> typeArgs, Formal k, List<Formal> formals,

                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                      Expression body, Attributes attributes, CoPredicate coPred)

-      : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {

+      : base(tok, name, isStatic, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {

       Contract.Requires(k != null);

       Contract.Requires(coPred != null);

       Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k);

@@ -2786,10 +2784,10 @@ namespace Microsoft.Dafny {
     public PrefixPredicate PrefixPredicate;  // filled in during resolution (name registration)

 

     public CoPredicate(IToken tok, string name, bool isStatic,

-                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,

+                     List<TypeParameter> typeArgs, List<Formal> formals,

                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens,

                      Expression body, Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(),

+      : base(tok, name, isStatic, true, typeArgs, formals, new BoolType(),

              req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureEllipsis) {

     }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ae998732..2edc7c3a 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -619,7 +619,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		IToken/*!*/ id;

 		Attributes attrs = null;

 		List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

-		IToken openParen;

 		List<Formal/*!*/> ins = new List<Formal/*!*/>();

 		List<Formal/*!*/> outs = new List<Formal/*!*/>();

 		List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

@@ -648,7 +647,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			if (la.kind == 45) {

 				GenericParameters(typeArgs);

 			}

-			Formals(true, true, ins, out openParen);

+			Formals(true, true, ins);

 			if (la.kind == 42 || la.kind == 43) {

 				if (la.kind == 42) {

 					Get();

@@ -656,11 +655,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 					Get();

 					SemErr(t, "iterators don't have a 'returns' clause; did you mean 'yields'?"); 

 				}

-				Formals(false, true, outs, out openParen);

+				Formals(false, true, outs);

 			}

 		} else if (la.kind == 44) {

 			Get();

-			signatureEllipsis = t; openParen = Token.NoToken; 

+			signatureEllipsis = t; 

 		} else SynErr(142);

 		while (StartOf(5)) {

 			IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);

@@ -878,10 +877,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Expression body = null;

 		bool isPredicate = false;  bool isCoPredicate = false;

 		bool isFunctionMethod = false;

-		IToken openParen = null;

 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		IToken signatureEllipsis = null;

+		bool missingOpenParen;

 		

 		if (la.kind == 67) {

 			Get();

@@ -899,13 +898,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				if (la.kind == 45) {

 					GenericParameters(typeArgs);

 				}

-				Formals(true, isFunctionMethod, formals, out openParen);

+				Formals(true, isFunctionMethod, formals);

 				Expect(7);

 				Type(out returnType);

 			} else if (la.kind == 44) {

 				Get();

-				signatureEllipsis = t;

-				openParen = Token.NoToken; 

+				signatureEllipsis = t; 

 			} else SynErr(148);

 		} else if (la.kind == 68) {

 			Get();

@@ -924,17 +922,19 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				if (la.kind == 45) {

 					GenericParameters(typeArgs);

 				}

+				missingOpenParen = true; 

 				if (la.kind == 16) {

-					Formals(true, isFunctionMethod, formals, out openParen);

-					if (la.kind == 7) {

-						Get();

-						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

-					}

+					Formals(true, isFunctionMethod, formals);

+					missingOpenParen = false; 

+				}

+				if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the predicate takes no additional arguments"); } 

+				if (la.kind == 7) {

+					Get();

+					SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

 				}

 			} else if (la.kind == 44) {

 				Get();

-				signatureEllipsis = t;

-				openParen = Token.NoToken; 

+				signatureEllipsis = t; 

 			} else SynErr(149);

 		} else if (la.kind == 69) {

 			Get();

@@ -949,17 +949,19 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				if (la.kind == 45) {

 					GenericParameters(typeArgs);

 				}

+				missingOpenParen = true; 

 				if (la.kind == 16) {

-					Formals(true, isFunctionMethod, formals, out openParen);

-					if (la.kind == 7) {

-						Get();

-						SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); 

-					}

+					Formals(true, isFunctionMethod, formals);

+					missingOpenParen = false; 

+				}

+				if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less co-predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the co-predicate takes no additional arguments"); } 

+				if (la.kind == 7) {

+					Get();

+					SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); 

 				}

 			} else if (la.kind == 44) {

 				Get();

-				signatureEllipsis = t;

-				openParen = Token.NoToken; 

+				signatureEllipsis = t; 

 			} else SynErr(150);

 		} else SynErr(151);

 		decreases = isCoPredicate ? null : new List<Expression/*!*/>(); 

@@ -975,13 +977,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		

 		IToken tok = theVerifyThisFile ? id : new IncludeToken(id);

 		if (isPredicate) {

-		  f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

+		  f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, formals,

 		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);

 		} else if (isCoPredicate) {

-		  f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, openParen, formals,

+		  f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, formals,

 		                    reqs, reads, ens, body, attrs, signatureEllipsis);

 		} else {

-		  f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

+		  f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, formals, returnType,

 		                   reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);

 		}

 		f.BodyStartTok = bodyStart;

@@ -1000,7 +1002,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		bool hasName = false;  IToken keywordToken;

 		Attributes attrs = null;

 		List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

-		IToken openParen;

 		List<Formal/*!*/> ins = new List<Formal/*!*/>();

 		List<Formal/*!*/> outs = new List<Formal/*!*/>();

 		List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();

@@ -1076,15 +1077,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			if (la.kind == 45) {

 				GenericParameters(typeArgs);

 			}

-			Formals(true, !mmod.IsGhost, ins, out openParen);

+			Formals(true, !mmod.IsGhost, ins);

 			if (la.kind == 43) {

 				Get();

 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

-				Formals(false, !mmod.IsGhost, outs, out openParen);

+				Formals(false, !mmod.IsGhost, outs);

 			}

 		} else if (la.kind == 44) {

 			Get();

-			signatureEllipsis = t; openParen = Token.NoToken; 

+			signatureEllipsis = t; 

 		} else SynErr(154);

 		while (StartOf(10)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

@@ -1396,10 +1397,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 	}

 

-	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {

-		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 

+	void Formals(bool incoming, bool allowGhostKeyword, List<Formal> formals) {

+		Contract.Requires(cce.NonNullElements(formals)); IToken id;  Type ty;  bool isGhost; 

 		Expect(16);

-		openParen = t; 

 		if (la.kind == 1 || la.kind == 32) {

 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

@@ -4039,7 +4039,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

-		{T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,x,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{T,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,x,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 2ec40e08..56722543 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -438,11 +438,7 @@ namespace Microsoft.Dafny {
       if (f.SignatureIsOmitted) {

         wr.WriteLine(" ...");

       } else {

-        if (f.OpenParen != null) {

-          PrintFormals(f.Formals, f.Name);

-        } else {

-          Contract.Assert(isPredicate);

-        }

+        PrintFormals(f.Formals, f.Name);

         if (!isPredicate) {

           wr.Write(": ");

           PrintType(f.ResultType);

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 5f116779..17867100 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -543,13 +543,13 @@ namespace Microsoft.Dafny
       }

 

       if (f is Predicate) {

-        return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

+        return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, formals,

           req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

       } else if (f is CoPredicate) {

-        return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

+        return new CoPredicate(tok, f.Name, f.IsStatic, tps, formals,

           req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

       } else {

-        return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, refinementCloner.CloneType(f.ResultType),

+        return new Function(tok, f.Name, f.IsStatic, isGhost, tps, formals, refinementCloner.CloneType(f.ResultType),

           req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

       }

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2cc6010a..8e5a7fd4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -879,7 +879,7 @@ namespace Microsoft.Dafny
             new Specification<Expression>(new List<Expression>(), null),

             null, null, null);

           // --- here comes predicate Valid()

-          var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(), iter.tok,

+          var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(),

             new List<Formal>(),

             new List<Expression>(),

             new List<FrameExpression>(),

@@ -950,7 +950,7 @@ namespace Microsoft.Dafny
 

                   // create prefix predicate

                   cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.IsStatic,

-                    tyvars, cop.OpenParen, k, formals,

+                    tyvars, k, formals,

                     cop.Req.ConvertAll(cloner.CloneExpr),

                     cop.Reads.ConvertAll(cloner.CloneFrameExpr),

                     cop.Ens.ConvertAll(cloner.CloneExpr),

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 90aee927..a8079bf9 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3399,9 +3399,7 @@ namespace Microsoft.Dafny {
       {

         var printer = new Printer(writer);

         printer.PrintAttributes(f.Attributes);

-        if (f.OpenParen != null) {

-          printer.PrintFormals(f.Formals);

-        }

+        printer.PrintFormals(f.Formals);

         writer.Write(": ");

         printer.PrintType(f.ResultType);

         printer.PrintSpec("", f.Req, 0);

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

     }