Contents

require 'contract'

class StackContract < Contract

  def push_post(stack_pre, stack, exception, result, element)
    assert_nil(result)
    assert_equal(element, stack.top)
    assert_equal(stack.size, stack_pre.size + 1)
  end

  def pop_pre(stack)
    assert_operator(stack.size, :>=, 0)
  end

  def pop_post(stack_pre, stack, exception, result)
    if stack_pre.empty?
      assert_kind_of(Stack::NoPopForEmptyStack, exception)
    else
      assert_equal(stack_pre.top, result)
      assert_equal(stack_pre.size - 1, stack.size)
    end
  end

  def top_pre(stack)
    assert_operator(stack.size, :>=, 1)
  end

  def top_post(stack_pre, stack, exception, result)
    assert_equal(stack_pre.size, stack.size)
  end

  def invariant(stack)
    assert_operator(stack.size, :>=, 0)
  end

end

Version data entries

2 entries across 2 versions & 1 rubygems

Version	Path
armin-joellenbeck-rdbc-0.0.4	examples/stack_contract.rb
armin-joellenbeck-rdbc-0.0.5	examples/stack_contract.rb