From dd99220a03dbb74d1191b68a9f8b0a6eb30b32ae Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 22 Apr 2013 13:52:13 -0700
Subject: Made Test/vstte2012/RingBuffer.dfy and
 Test/dafny1/ExtensibleArray.dfy more similar to RingBufferAuto.dfy and
 ExtensibleArrayAuto.dfy, respectively, so that the effect of {:autocontracts}
 is more easily seen.

---
 Test/dafny1/ExtensibleArray.dfy | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index a16cf603..adf97863 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -7,7 +7,7 @@ class ExtensibleArray<T> {
   var length: int;
   var M: int;  // shorthand for:  if more == null then 0 else 256 * |more.Contents|
 
-  function Valid(): bool
+  predicate Valid()
     reads this, Repr;
   {
     // shape of data structure
@@ -17,21 +17,21 @@ class ExtensibleArray<T> {
         more in Repr && more.Repr <= Repr && this !in more.Repr && elements !in more.Repr &&
         more.Valid() &&
         |more.Contents| != 0 &&
-        forall j :: 0 <= j && j < |more.Contents| ==>
+        forall j :: 0 <= j < |more.Contents| ==>
             more.Contents[j] != null && more.Contents[j].Length == 256 &&
             more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&
             more.Contents[j] != elements &&
-            forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
+            forall k :: 0 <= k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
 
     // length
     M == (if more == null then 0 else 256 * |more.Contents|) &&
-    0 <= length && length <= M + 256 &&
+    0 <= length <= M + 256 &&
     (more != null ==> M < length) &&
 
     // Contents
     length == |Contents| &&
-    (forall i :: 0 <= i && i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
-    (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])
+    (forall i :: 0 <= i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
+    (forall i :: M <= i < length ==> Contents[i] == elements[i - M])
   }
 
   constructor Init()
@@ -50,7 +50,7 @@ class ExtensibleArray<T> {
 
   method Get(i: int) returns (t: T)
     requires Valid();
-    requires 0 <= i && i < |Contents|;
+    requires 0 <= i < |Contents|;
     ensures t == Contents[i];
     decreases Repr;
   {
@@ -64,7 +64,7 @@ class ExtensibleArray<T> {
 
   method Set(i: int, t: T)
     requires Valid();
-    requires 0 <= i && i < |Contents|;
+    requires 0 <= i < |Contents|;
     modifies Repr;
     ensures Valid() && fresh(Repr - old(Repr));
     ensures Contents == old(Contents)[i := t];
-- 
cgit v1.2.3