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

11 files changed, 39 insertions, 40 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

   }

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 {

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 74512e01..21b895aa 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,6 +1,6 @@
 // Celebrity example, inspired by the Rodin tutorial

 

-static function method Knows<Person>(a: Person, b: Person): bool;

+static function method Knows<Person>(a: Person, b: Person): bool

   requires a != b;  // forbid asking about the reflexive case

 

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

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index fdce6dc7..39e14ea5 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -163,7 +163,7 @@ function mapF(xs: List): List
   case Nil => Nil

   case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))

 }

-function HardcodedUninterpretedFunction(n: Nat): Nat;

+function HardcodedUninterpretedFunction(n: Nat): Nat

 

 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

@@ -195,7 +195,7 @@ function filterP(xs: List): List
     then Cons(y, filterP(ys))

     else filterP(ys)

 }

-function HardcodedUninterpretedPredicate(n: Nat): Bool;

+function HardcodedUninterpretedPredicate(n: Nat): Bool

 

 function insort(n: Nat, xs: List): List

 {

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 189ff2b5..c8419890 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -29,7 +29,7 @@ class UltraFilter<G> {
   }

 

   // Dafny currently does not have a set comprehension expression, so this method stub will have to do

-  method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);

+  method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)

     ensures (forall X :: X in h <==> M + X in f);

 

   method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)