Dafny: added ghost modules (the meaning is simply that such a module will not be compiled)

Dafny: improved :autocontracts heuristic for detecting "simple query method"
Dafny: fixed some bugs

1 files changed, 15 insertions, 16 deletions

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index 49f76713..b02022c7 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -1,11 +1,15 @@
 class {:autocontracts} RingBuffer<T>

 {

-  // public fields that are used to define the abstraction:

+  // public view of the class:

   ghost var Contents: seq<T>;  // the contents of the ring buffer

   ghost var N: nat;  // the capacity of the ring buffer

 

-  // Valid encodes the consistency of RingBuffer objects (think, invariant).

-  // An explanation of this idiom is explained in the README file.

+  // private implementation:

+  var data: array<T>;

+  var first: nat;

+  var len: nat;

+

+  // Valid encodes the consistency of RingBuffer objects (think, invariant)

   predicate Valid

   {

     data != null &&

@@ -16,11 +20,6 @@ class {:autocontracts} RingBuffer<T>
                                     else data[first..] + data[..first+len-N]

   }

 

-  // private implementation:

-  var data: array<T>;

-  var first: nat;

-  var len: nat;

-

   constructor Create(n: nat)

     ensures Contents == [] && N == n;

   {

@@ -43,7 +42,7 @@ class {:autocontracts} RingBuffer<T>
     x := data[first];

   }

 

-  method Push(x: T)

+  method Enqueue(x: T)

     requires |Contents| != N;

     ensures Contents == old(Contents) + [x] && N == old(N);

   {

@@ -54,7 +53,7 @@ class {:autocontracts} RingBuffer<T>
     Contents := Contents + [x];

   }

 

-  method Pop() returns (x: T)

+  method Dequeue() returns (x: T)

     requires Contents != [];

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

   {

@@ -67,10 +66,10 @@ class {:autocontracts} RingBuffer<T>
 method TestHarness(x: int, y: int, z: int)

 {

   var b := new RingBuffer<int>.Create(2);

-  b.Push(x);

-  b.Push(y);

-  var h := b.Pop();  assert h == x;

-  b.Push(z);

-  h := b.Pop();  assert h == y;

-  h := b.Pop();  assert h == z;

+  b.Enqueue(x);

+  b.Enqueue(y);

+  var h := b.Dequeue();  assert h == x;

+  b.Enqueue(z);

+  h := b.Dequeue();  assert h == y;

+  h := b.Dequeue();  assert h == z;

 }