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

3 files changed, 23 insertions, 24 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 3de94555..7cf3de07 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -12,13 +12,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];

@@ -33,7 +33,7 @@ class Queue<T> {
 }

 

 class Comparable {

-  function AtMost(c: Comparable): bool;

+  function AtMost(c: Comparable): bool

     reads this, c;

 }

 

@@ -96,7 +96,6 @@ class Benchmark3 {
   }

   

   

-

   method RemoveMin(q: Queue<int>) returns (m: int, k: int) //m is the min, k is m's index in q

     requires q != null && |q.contents| != 0;

     modifies q;

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);

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 0c9d1186..383bccfd 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -6,13 +6,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];

@@ -28,7 +28,7 @@ class Queue<T> {
 

 

 class Glossary {

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

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

     requires q != null;

     modifies q;

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

@@ -149,29 +149,29 @@ class Glossary {
   

 class Word

 {

-  function AtMost(w:Word) :bool;

+  function AtMost(w: Word): bool

 }

   

 class ReaderStream {

-  ghost var footprint:set<object>;

-  var isOpen:bool;

+  ghost var footprint: set<object>;

+  var isOpen: bool;

   

-  function Valid():bool

-  reads this, footprint;

+  function Valid(): bool

+    reads this, footprint;

   {

     null !in footprint && this in footprint && isOpen

   }

   

   method Open() //reading

-  modifies this;

-  ensures Valid() && fresh(footprint -{this});

+    modifies this;

+    ensures Valid() && fresh(footprint -{this});

   {

     footprint := {this}; 

     isOpen :=true;

   }

   

-  method GetWord()returns(x:Word)

-    requires Valid() ;

+  method GetWord() returns (x: Word)

+    requires Valid();

     modifies footprint;

     ensures Valid() && fresh(footprint - old(footprint));

   {

@@ -190,8 +190,8 @@ class WriterStream {
   var stream:seq<int>; 

   var isOpen:bool;

   

-  function Valid():bool

-  reads this, footprint;

+  function Valid(): bool

+    reads this, footprint;

   {

     null !in footprint && this in footprint && isOpen

   }