interface IntList {
  var list: seq[int]

  constructor Empty()
    ensures list = []

  constructor SingletonTwo()
    ensures list = [2]

  constructor OneTwo()
    ensures list = [1 2]

  constructor Singleton(p: int)
    ensures list = [p]

  constructor TwoConsecutive(p: int)
    ensures list = [p] + [p+1]

  constructor Double(p: int, q: int)
    ensures list = [p] + [q]

  constructor Sum(p: int, q: int)
    ensures list = [p + q]
}

datamodel IntList {
  var root: IntNode

  frame
    root

  invariant
    root = null <==> |list| = 0
    root != null ==> list = root.list
}

interface IntNode {
  var list: seq[int]

  invariant
    |list| > 0

  constructor SingletonZero()
    ensures list = [0]

  constructor Init(x: int) 
    ensures list = [x]

  constructor Double(x: int, y: int)
    ensures list = [x y]
	
  method Max() returns (ret: int)
    ensures ret in list
	ensures forall t :: t in list ==> ret >= t

}

datamodel IntNode {
  var data: int
  var next: IntNode

  frame 
    next

  invariant
    next = null ==> list = [data]
    next != null ==> list = [data] + next.list
}