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

1 files changed, 4 insertions, 4 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;