booger (master)$ cat examples/example3.rb
class Stack
  # @modifies @elements
  # @modifies @size
  def initialize
    @size = 0
    # @elements = [] (array assignment not yet supported)
  end

  # @modifies @elements
  # @modifies @size
  # @ensures @size == old(@size) + 1
  def push(element)
    @size = @size + 1
    @elements.push element
  end

  # @modifies @size
  # @requires @size > 0
  # @ensures @size == old(@size) - 1
  def pop
    @size = @size - 1
    @elements.pop
  end
end

def use
  stack = Stack.new
  stack.pop
end

booger (master)$ ./bin/booger examples/example3.rb
Verification Errors (2):

- A precondition for this call might not hold:31:
      stack.pop

- This is the precondition that might not hold:
      @requires @size > 0