1 files changed, 0 insertions, 40 deletions
diff --git a/Test/jennisys0/ExtensibleArray.jen b/Test/jennisys0/ExtensibleArray.jen
deleted file mode 100644
index 7ef36ce2..00000000
--- a/Test/jennisys0/ExtensibleArray.jen
+++ /dev/null
@@ -1,40 +0,0 @@
-class ExtensibleArray[T] {
-  var Contents: seq[T]
-
-  constructor Init()
-    Contents := []
-
-  method Get(i) returns (t)
-    requires 0 <= i && i < |Contents|
-    t := Contents[i]
-
-  method Set(i, t)
-    requires 0 <= i && i < |Contents|
-    Contents := Contents[i := t]
-
-  method Append(t)
-    Contents := Contents + [t]
-}
-
-model ExtensibleArray[T] {
-  var elements: array[T]
-  var more: ExtensibleArray[array[T]]
-  var length: int
-  var M: int
-
-  frame
-    elements * more * more.Contents[*]
-
-  invariant
-    elements != null
-    elements.Length = 256
-    more = null ==> M = 0
-    more != null ==> |more.Contents| != 0 && M = 256 * |more.Contents|
-    0 <= length && length <= M + 256
-    more != null ==> M < length
-
-    length = |Contents|
-    more != null ==> forall i :: 0 <= i && i < |more.Contents| ==> more.Contents[i] != null && more.Contents[i].Length = 256
-    more != null ==> forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
-    forall i :: M <= i && i < length ==> Contents[i] = elements[i - M]
-}