// Design by Contract in Nex
class Stack<T>

  fn push(value: T)
    requires !is_full()
    ensures  count == old_count + 1
  end

  fn pop() → T
    requires count > 0
  end

end