From e84cd11c77d9d93429ee175b4008d3893ecfe7df Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 7 Mar 2012 13:13:22 -0800
Subject: 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

---
 Test/vstte2012/RingBufferAuto.dfy | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

(limited to 'Test/vstte2012')

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