class StackContract < Rdbc::Contract

  post :push do |stack_pre, stack, exception, result, element|
    assert(result.nil?)
    assert(stack.top == element)
    assert(stack.size ==stack_pre.size + 1)
  end

  pre :pop do |stack|
    assert(stack.size >= 1)
  end

  post :pop do |stack_pre, stack, exception, result|
    assert(result.nil?)
    assert(stack_pre.size - 1 == stack.size)
  end

  pre :top do |stack|
    assert(stack.size >= 1)
  end

  post :top do |stack_pre, stack, exception, result|
    assert(stack_pre.size == stack.size)
  end

  invariant do |stack|
    assert(stack.size >= 0)
  end

end


class Stack

  contract StackContract

  def initialize
    @objects = []
  end

  def initialize_copy(orig)
    @objects = orig.objects
  end

  def objects
    @objects.dup
  end

  def size
    @objects.size
  end

  def empty?
    size == 0
  end

  def top
    @objects.last
  end

  def pop
    @objects.pop
    nil
  end

  def push(object)
    @objects.push(object)
    nil
  end

end


describe 'A new Stack' do
  before do
    @stack = Stack.new
  end

  it 'should be empty.' do
    @stack.empty?
  end

  it 'should have no object on its top' do
     lambda{@stack.top}.should raise_error(Rdbc::Contract::AssertionFailed)
  end

  it 'should be so that no object can be popped' do
     lambda{@stack.pop}.should raise_error(Rdbc::Contract::AssertionFailed)
  end

  it 'A pushed object should be on the top' do
    object = Object.new
    @stack.push(object)
    @stack.top.should equal(object)
  end
end