Dafny: allow constructors only inside classes, removed semi-colons at end of body-less functions/methods

5 files changed, 12 insertions, 12 deletions

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 8df1a7c5..2063eec4 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -44,17 +44,17 @@ class SoWellformed {
     c := true;

   }

 

-  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);

+  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

     requires next != null;

     modifies this;

     ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

 

-  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)

     requires next != null;

     modifies s;

     ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

 

-  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)

     requires next != null && this !in s;

     modifies s;

     ensures next.xyz < 100;  // fine

@@ -175,7 +175,7 @@ class StatementTwoShoes {
   }

 

   function G(w: int): int { 5 }

-  function method H(x: int): int;

+  function method H(x: int): int

 

   method V(s: set<StatementTwoShoes>, a: int, b: int)

     modifies s;

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 53d3bf03..e56b4122 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -42,7 +42,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
   r := t1;

 }

 

-function method FenEric<T>(t0: T, t1: T): T;

+function method FenEric<T>(t0: T, t1: T): T

 

 datatype Pair<T> = Pr(T, T);

 

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index d4d1dfcf..f31935af 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -87,7 +87,7 @@ class Termination {
     }

   }

 

-  method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);

+  method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)

     requires a != List.Nil;

     ensures a == List.Cons(val, b);

 }

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 2bedd37d..710e9838 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -88,7 +88,7 @@ method N() returns (k: MyClass)
   k := new MyClass;

 }

 

-function NF(): MyClass;

+function NF(): MyClass

 

 function TakesADatatype(a: List): int { 12 }

 

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a3698dc0..8f3f8b87 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -17,7 +17,7 @@ class C<U> {
     assert kz && (G() || !G());

   }

 

-  function G<Y>(): Y;

+  function G<Y>(): Y

 }

 

 class SetTest {

@@ -99,7 +99,7 @@ class CClient {
 

 // -------------------------

 

-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;

+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool

   requires c == c || c in people;

 

 method FindCelebrity3(people: set<int>, ghost c: int)

@@ -110,7 +110,7 @@ method FindCelebrity3(people: set<int>, ghost c: int)
   b := F(c, people);

 }

 

-static function F(c: int, people: set<int>): bool;

+static function F(c: int, people: set<int>): bool

   requires IsCelebrity(c, people);

 

 function RogerThat<G>(g: G): G

@@ -153,8 +153,8 @@ method LoopyRoger(n: int)
 

 class TyKn_C<T> {

   var x: T;

-  function G(): T;

-  method M() returns (t: T);

+  function G(): T

+  method M() returns (t: T)

 }

 

 class TyKn_K {