From eacaf0b44276f0a61d6cc4204bb4d48d02fc0548 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 11 Jul 2011 19:08:48 -0700
Subject: Dafny: allow constructors only inside classes, removed semi-colons at
 end of body-less functions/methods

---
 Test/VSI-Benchmarks/b3.dfy |  9 ++++-----
 Test/VSI-Benchmarks/b7.dfy |  8 ++++----
 Test/VSI-Benchmarks/b8.dfy | 30 +++++++++++++++---------------
 3 files changed, 23 insertions(+), 24 deletions(-)

(limited to 'Test/VSI-Benchmarks')

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
   }
-- 
cgit v1.2.3