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]
}