future.cr

require "crystal-clear"

class FooBar
  invariants do
    @val != nil
  end

  def initialize(@val = nil)
    @val = 5
  end

  test do 
    val > 0 # Becomes a require
    def test_method(val)
      100 / val + 1
    end
    return_value > 0 # Becomes an ensure
  end

  test do
    val > 0
    def bad_method(val)
      @val = nil # Will throw an exception because this is not okay!
      100 / val + 1
    end
    return_value > 0
  end

  def break_internally
    @val = nil # Will throw an exception because this is not okay! 
  end

  def fixes_internally
    break_internally 
    @val = 5 # Invariants are only run when you leave the object completly so this is fine
  end
end

right_now.cr

require "crystal-clear"

class FooBar
  invariant(@val != nil)

  def initialize(@val = nil)
    @val = 5
  end

  requires(test_method(val), val > 0)
  ensures(test_method(val), return_value > 0)
  def test_method(val)
    100 / val + 1
  end

  requires(bad_method(val), val > 0)
  ensures(bad_method(val), return_value > 0)
  def bad_method(val)
    @val = nil # Will throw an exception because this is not okay!
    100 / val + 1
  end

  enforce_contracts(break_internally)
  def break_internally
    @val = nil # Will throw an exception because this is not okay! 
  end

  enforce_contracts(fixes_internally)
  def fixes_internally
    break_internally 
    @val = 5 # Invariants are only run when you leave the object completly so this is fine
  end
end