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/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index f34f5c00..d6759c5f 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -8,13 +8,13 @@
 

 class Queue<T> {

   var contents: seq<T>;

-  method Init();

+  method Init()

     modifies this;

     ensures |contents| == 0;

-  method Enqueue(x: T);

+  method Enqueue(x: T)

     modifies this;

     ensures contents == old(contents) + [x];

-  method Dequeue() returns (x: T);

+  method Dequeue() returns (x: T)

     requires 0 < |contents|;

     modifies this;

     ensures contents == old(contents)[1..] && x == old(contents)[0];

@@ -101,7 +101,7 @@ class Stream {
 

 

 class Client {

-  method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);

+  method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)

     requires q != null;

     modifies q;

     ensures r != null && fresh(r);