From 3e6b9ca45da9eba02cf1cba553b129fd039f03df Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 19 Nov 2012 07:45:36 -0800
Subject: Beautified a test program

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

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index f7f97deb..3e91fa4b 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -6,7 +6,7 @@ class {:autocontracts} ExtensibleArray<T> {
   var length: int;
   var M: int;  // shorthand for:  if more == null then 0 else 256 * |more.Contents|
 
-  function Valid(): bool
+  predicate Valid()
   {
     // shape of data structure
     elements != null && elements.Length == 256 &&
@@ -14,21 +14,21 @@ class {:autocontracts} ExtensibleArray<T> {
         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()
@@ -43,7 +43,7 @@ class {:autocontracts} ExtensibleArray<T> {
   }
 
   method Get(i: int) returns (t: T)
-    requires 0 <= i && i < |Contents|;
+    requires 0 <= i < |Contents|;
     ensures t == Contents[i];
     decreases Repr;
   {
@@ -56,7 +56,7 @@ class {:autocontracts} ExtensibleArray<T> {
   }
 
   method Set(i: int, t: T)
-    requires 0 <= i && i < |Contents|;
+    requires 0 <= i < |Contents|;
     ensures Contents == old(Contents)[i := t];
   {
     if (M <= i) {
-- 
cgit v1.2.3