Contracts fail when a method is redefined (overridden) in a subclass

[jjttcc]

I wrote some simple test code to try out ruby_contracts with inheritance and am getting an error in a redefined method (in SimpleChild, subclass of Simple) where the method in the parent has a precondition and postcondition. My code is inserted below. The redefined method is multiplied_by. I get an error both when defining a new precondition for the method in the subclass and when this precondition is commented out. The errors messages for these two cases are different, but very similar - it appears to be the same cause.

The error message with the subclass precondition is:

/usr/local/share/gems/gems/ruby_contracts-0.1.1/lib/ruby_contracts.rb:27:in `pre': undefined method `[]' for nil:NilClass (NoMethodError)
from /tmp/work/simplechild.rb:4:in `<class:SimpleChild>'
from /tmp/work/simplechild.rb:3:in `<top (required)>'
from ./test-simplechild1.rb:3:in `require_relative'
from ./test-simplechild1.rb:3:in `<main>'

and without the precondition:

/usr/local/share/gems/gems/ruby_contracts-0.1.1/lib/ruby_contracts.rb:35:in `method_added': undefined method `[]' for nil:NilClass (NoMethodError)
from /tmp/work/simplechild.rb:7:in `<class:SimpleChild>'
from /tmp/work/simplechild.rb:3:in `<top (required)>'
from ./test-simplechild1.rb:3:in `require_relative'
from ./test-simplechild1.rb:3:in `<main>'

I believe this is a bug. Note: If I remove the multiplied_by method definition in SimpleChild, the test script runs without the error.

By the way, I like this module - it seems well designed and well implemented, and I especially like that assertion checking can be disabled. Hopefully this bug is relatively easy to fix. Thanks!

[simple.rb]

require 'ruby_contracts'

class Simple
  include Contracts::DSL
  EPSILON = 1e-7
  attr_reader :value

  type :in => [Numeric]
  pre  "val >= 0" do |val| val >= 0 end
  post "value set" do |val| @value == val end
  def initialize(val)
    @value = val
  end

  type :in => [Numeric], :out => Numeric
  pre  "n < self.value" do |n| n < @value end
  post "result = n * self.value" do |result, n|
    x = 0; for i in 1..n do x += @value end
    puts "x, result: #{x}, #{result}; x == result: #{x - result < 1e-4}"; x - result < EPSILON
  end
  def multiplied_by(n)
    @value * n
  end
end


[simplechild.rb]

require_relative 'simple'

class SimpleChild < Simple
#  pre  "n < self.value + 100" do |n| n < @value + 100 end
# [The undefined method error occurs with the above precondition both
# commented out and uncommented.]
  def multiplied_by(n)
    @value * n
  end
end


[test-simplechild1.rb]

#!/bin/env ruby

require_relative 'simplechild'

e = SimpleChild.new(77)
puts "test1:"
begin
  puts e.multiplied_by(6)
rescue Exception => x
  puts x
end
puts "test2:"
begin
  puts e.multiplied_by(77)
rescue Exception => x
  puts "#{x} [#{x.class}]"
  puts x.backtrace.inspect
end
puts "test3:"
begin
  e = SimpleChild.new(-3)
  puts e.multiplied_by(99)
rescue Exception => x
  puts "#{x} [#{x.class}]"
  puts x.backtrace.inspect
end

[nicoolas25]

Thank you for testing ruby_contracts.

I did not built any support for class inheritance because the project was initially a proof of concept. Today, I've just added this new feature with a quick patch. In the future, I'll refactor the existing design in a more maintainable way. If you have other ideas or contributions, do not hesitate to tell me about it.

Be aware that adding a new precondition in the SimpleChild class on the multiply_by method will not remove the superclass's preconditions. An instance of SimpleChild should be able to replace an instance of Simple without breaking any contracts.

[jjttcc]

Nicolas - Thanks much for the rapid response and fix. I've tested the new version and verified that the original problem is fixed - the "undefined method" error no longer occurs and the pre- and post-conditions are checked for a subclass that inherits a method with a contract.

However, it appears that there's an error in the logic for inherited preconditions: if an inherited method with a precondition is redefined with an additional precondition, when the subclass precondition is checked it is "and"ed with the inherited precondition, effectively making the resulting entire precondition for the inherited method stronger than in the parent. The precondition should actually be weaker - that is, it should be "or"ed with the parent precondition. (Your statement "An instance of SimpleChild should be able to replace an instance of Simple without breaking any contracts." is correct and compatible with the "or"ing interpretation.) [See, e.g.:
http://en.wikipedia.org/wiki/Precondition#Preconditions_and_inheritance .]

I had a look at your code to see if I could implement a fix, but I'm pretty inexperienced with ruby and your code is quite advanced, so I gave up.

By the way, postconditions are also "and"ed in your implementation, which is correct. (e.g.:
http://en.wikipedia.org/wiki/Postcondition#Postconditions_and_inheritance .)

I put together a small test case (a further simplified version of the test code I initially posted) to illustrate the problem. I'll include this code in a followup.

Thanks!

[jjttcc]

Here is the test code I promised. I simply added the precondition 'true' in the inherited version of 'multiplied_by' in SimpleChild. In the test, e.multiplied_by(6) should pass the precondition, since the complete preconditiion is:
'n < value or true', which is always true. Instead, the precondition fails because the two conditions are "and"ed - e.g.: '6 < 6 and true'.

basic_test.rb:

#!/bin/env ruby

require_relative 'simplechild'

e = SimpleChild.new(6)
puts "6 * 5: #{e.multiplied_by(5)}"
begin
  puts "6 * 6: #{e.multiplied_by(6)}"
rescue Exception => x
  puts x
  puts x.backtrace
end

simple.rb:

require 'ruby_contracts'

class Simple
  include Contracts::DSL
  EPSILON = 1e-7
  attr_reader :value

  type :in => [Numeric]
  pre  "val >= 0" do |val| val >= 0 end
  post "value set" do |val| value == val end
  def initialize(val)
    @value = val
  end

  type :in => [Numeric], :out => Numeric
  pre  "n < self.value" do |n| n < value end
  post "result = n * self.value" do |result, n|
    x = 0; (1..n).each do x += value end; (x - result).abs < EPSILON
  end
  def multiplied_by(n)
    value * n
  end
end

simplechild.rb:

require_relative 'simple'

class SimpleChild < Simple
  pre  "true" do true end
  def multiplied_by(n)
    @value * n
  end
end

[nicoolas25]

I've modified the pre/post-conditions inheritance behavior as you suggested in the version 0.2.3.

When there is no preconditions, should the expected behavior be:

• no precondition at all or
• the same preconditions as the parent class ?

[jjttcc]

Hi Nicolas - Again, I'm impressed with your quick response on this. (Are
you in France?)

Re. when there is no precondition defined in a subclass method -
redefinition of the parent method - in this case the precondition from the
parent class is inherited as is. The idea is that the subclass has to
fulfill the contract promised by the parent (since a user of the class is
justified as regarding it, contractwise, as an instance of the parent) and
when no additional precondition is specified in the subclass, inheriting
the precondition as is upholds the contract. The precondition can only be
changed in the subclass method by explicitly defining one, in which case
any conditions added in the subclass will be "or"ed with the preconditions
inherited from the parent. So the subclass can weaken an inherited
precondition (thus not demanding anything further from a user of the
class/method), but there's no way to strengthen the precondition. And, of
course, if the subclass author wants no precondition at all (i.e., any
state will satisfy the precondition), he can just do: 'pre "true" do true
end' (as in my test case) to specify this.

I plan on testing your latest changes some time today, and will let you
know the results.

Thanks!
Jim

On Thu, Jun 13, 2013 at 3:25 AM, Nicolas Zermati
[email protected]:

I've modified the pre/post-conditions inheritance behavior as you
suggested in the version 0.2.3.

When there is no preconditions, should the expected behavior be:

• no precondition at all or
• the same preconditions as the parent class ?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/1#issuecomment-19378387
.

[jjttcc]

Hi Nicolas -

I just forked/branched some tests that show a couple remaining bugs and
created a pull request for your project. I'm sure you'll receive a
notification about this, but I thought I'd give you a heads up here, since
it's about this same issue - inherited pre/postconditions.

Let me know if you have any questions, etc.

Thanks!
Jim

On Thu, Jun 13, 2013 at 3:25 AM, Nicolas Zermati
[email protected]:

I've modified the pre/post-conditions inheritance behavior as you
suggested in the version 0.2.3.

When there is no preconditions, should the expected behavior be:

• no precondition at all or
• the same preconditions as the parent class ?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/1#issuecomment-19378387
.

[nicoolas25]

I've fixed the code to pass most of your examples. Could you tell me if you find remaining issues about inheritance in version 0.2.4 ?

[jjttcc]

Nicolas -

I ran all of the tests I've created for ruby_contracts and the only ones
that failed were the following:

• The postcondition tests in the postbug directory I created fail (test
  scripts testparent.rb and testchild.rb). The postcondition is actually
  maintained ("@value == v && @minimum_incr == mininc") but it is reported as
  violated. Since simple postconditions work fine, I suspect there is an
  error in how a compound postcondition like this one is handled. I would
  give this issue the highest priority, by far.
• An input type error is not detected when a method has, in addition to a
  type spec, a pre and/or postcondition. Instead, an error caused by the
  wrong type is triggered later, when the method runs (e.g.: 'comparison of
  String with 0 failed'). [I've created a test specifically for this. Let
  me know if you'd like me to send the files to you.]

So of the 3 problems I reported last time ("wrong # of arguments" reported
instead of precondition error message; precondition violation not detected
in inherited method that is overridden but no preconditions are added in
the subclass; and some postcondition violations are incorrectly reported)
only the last one, the postcondition problem, appears to not be fixed yet.

I also discovered a minor bug - if class B, subclass of A, has a redefined
method, m, with an additional precondition, if a precondition violation for
m occurs on a B object, the error message reports the string specified for
the parent precondition, not the one in the subclass. (Ideally, they
should probably both be reported.) I don't know if this bug shows up with
every such case, but I suspect it does. This I'd rate as low priority, but
it'd be nice if it could be fixed at some point.

On Fri, Jun 14, 2013 at 4:42 AM, Nicolas Zermati
[email protected]:

I've fixed the code to pass most of your examples. Could you tell me if
you find remaining issues about inheritance in version 0.2.4 ?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/1#issuecomment-19448087
.

[nicoolas25]

Post-conditions blocs take the result of the method as first argument then all the arguments passed to it. For instance: do |v, mininc| @value == v && @minimum_incr == mininc end is wrong. It should be: do |result, v, mininc| @value == v && @minimum_incr == mininc end.

[nicoolas25]

An input type error is not detected when a method has, in addition to a type spec, a pre and/or postcondition.
Instead, an error caused by the wrong type is triggered later, when the method runs (e.g.: 'comparison of String with 0 failed').

Of course if you have a non working example for this, I'll be happy to see it and add it to the test suite.

[nicoolas25]

An input type error is not detected when a method has, in addition to a type spec, a pre and/or postcondition.
Instead, an error caused by the wrong type is triggered later, when the method runs (e.g.: 'comparison of String with 0 failed').

It's ok, I found this one.

[nicoolas25]

An input type error is not detected when a method has, in addition to a type spec, a pre and/or postcondition.
Instead, an error caused by the wrong type is triggered later, when the method runs (e.g.: 'comparison of String with 0 failed').

I released the version 0.2.5 that will fix this issue.

[nicoolas25]

I opened an issue #3 to answer the last part of your message.

[jjttcc]

You're right - about postconditions/result. So the problem in this case
was user error, not a bug. However, it might be a good idea to add
something about this in the documentation/README. The confusion I had was
(although I'd caught on earlier from your example that result is the first
argument) I forgot about 'result' in 'initialize' since 'initialize'
doesn't return a result. (Or perhaps it's more accurate to say that the
result for 'initialize' is always ignored.) I suspect others would run
into this same confusion.

On Sat, Jun 15, 2013 at 2:38 AM, Nicolas Zermati
[email protected]:

Post-conditions blocs take the result of the method as first argument then
all the arguments passed to it. For instance: do |v, mininc| @value == v
&& @minimum_incr == mininc end is wrong. It should be: do |result, v,
mininc| @value == v && @minimum_incr == mininc end.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/1#issuecomment-19492753
.

[nicoolas25]

The README could be improved, I give you that :-) I'll make something more appealing in the future.