From 60208673a25423e378cc7e9672d5acf9fd6f58bc Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Mon, 7 Jul 2014 15:09:33 -0700
Subject: New logical encoding of types with Is and IsAlloc

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

(limited to 'Test/vacid0')

diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
index 06fca9f0..1e54f02f 100644
--- a/Test/vacid0/SparseArray.dfy
+++ b/Test/vacid0/SparseArray.dfy
@@ -40,8 +40,8 @@ class SparseArray<T> {
     ensures |Contents| == N && this.zero == zero;
     ensures (forall x :: x in Contents ==> x == zero);
   {
-    var aa := AllocateArray(N);  this.a := aa;
-    var bb := AllocateArray(N);  this.b := bb;
+    var aa : seq<T> := AllocateArray(N);  this.a := aa;
+    var bb : seq<int> := AllocateArray(N);  this.b := bb;
     bb := AllocateArray(N);  this.c := bb;
     this.n := 0;
 
@@ -101,19 +101,20 @@ class SparseArray<T> {
     Contents := Contents[i := x];
   }
 
-  /* The following method is here only to simulate support of arrays in Dafny */
-  /*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
-    requires 0 <= n;
-    ensures |arr| == n;
+}
+
+/* The following method is here only to simulate support of arrays in Dafny */
+/*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
+  requires 0 <= n;
+  ensures |arr| == n;
+{
+  arr := [];
+  var i := 0;
+  while (i < n)
+    invariant i <= n && |arr| == i;
   {
-    arr := [];
-    var i := 0;
-    while (i < n)
-      invariant i <= n && |arr| == i;
-    {
-      var g: G;
-      arr := arr + [g];
-      i := i + 1;
-    }
+    var g: G;
+    arr := arr + [g];
+    i := i + 1;
   }
 }
-- 
cgit v1.2.3