-------------------- Prog0.jen --------------------
// Jennisys, Copyright (c) 2011, Microsoft.
---------- Given Jennisys program ----------
class C {
  var a: seq[int]
  var x: int
  constructor Init()
  method Update(d)
    x := x + 1
    {
      nested := statement
      yes := sirrie
    }
    x.f := (12 + true)[8000 := 0 <= n]
  method Query() returns (r)
    requires r
    requires a[*]
    requires r.r.s
    requires a[i]
    requires a[i := 58]
    requires hello
    requires (hello + goodbye) - soonyousoon
    requires 0 <= r
    {
    }
  method ManyParams(x: bool, y) returns (r, s: set[MyClass], t)
}
model C {
  var x: int
  var q: bool
  frame
    xyz
    abc
    klm
    mno
    pqr
    a
    b
    c
  invariant
    x <= x
    x < 100
    y < 1000
}
code C {
}
----------

-------------------- ExtensibleArray.jen --------------------
// Jennisys, Copyright (c) 2011, Microsoft.
---------- Given Jennisys program ----------
class ExtensibleArray[T] {
  var Contents: seq[T]
  constructor Init()
    Contents := []
  method Get(i) returns (t)
    requires 0 <= i
    requires i < |Contents|
    t := Contents[i]
  method Set(i, t)
    requires 0 <= i
    requires 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]
}
----------