Invariant Issue

[Steve]

I was coding some of the Head First Design Patterns examples in Cobra, but with contracts and unit tests when I ran into a bit of an issue with invariants. Here is the code:

# --------------------------------------------------

class Beverage
    is abstract
    
    get description as String
        ensure
            result.length > 0
        body
            return 'Unknown Beverage'

    get cost as decimal is abstract

    invariant
        .cost > 0.0

# --------------------------------------------------

class CondimentDecorator
    is abstract
    inherits Beverage

    var _beverage as Beverage

    pro beverage as Beverage is protected
        get
            return _beverage
        set
            _beverage = value

    get description as String is override, abstract

    def init(beverage as Beverage)
        .beverage = beverage

# --------------------------------------------------

class Espresso
    inherits Beverage

    get description as String is override
        return 'Espresso'

    get cost as decimal is override
        return 1.99

    test
        b as Beverage = Espresso()
        assert b.description == 'Espresso'
        assert b.cost == 1.99

# --------------------------------------------------

class Mocha
    inherits CondimentDecorator

    get description as String is override
        return '[.beverage.description], Mocha' 

    get cost as decimal is override
        return 0.20 + .beverage.cost

    def init(beverage as Beverage)
        base.init(beverage)

    test
        b as Beverage = Espresso()
        b = Mocha(b)
        assert b.description == 'Espresso, Mocha'
        assert b.cost == 1.99 + 0.20

The test in Mocha fails because when the constructor in the abstract class CondimentDecorator is called, at the end of that constructor the invariant from the parent class (Beverage) is not satisfied. Two questions arise:
1) Should the invariant be called after CondimentDecorator's constructor? It would seem that all invariant checking should be delayed until the end of the original constructor.
2) For me, using Cobra 0.8.0, this problem resulted in an unhandled null reference exception. If invariant handling should operate in this fashion, it would seem that this should be handled in a cleaner fashion.

Let me know and best regards as always,


Steve

--

[Charles]

1) Should the invariant be called after CondimentDecorator's constructor? It would seem that all invariant checking should be delayed until the end of the original constructor.

That's an interesting question especially with the ancestor classes being abstract. I have to think about it some more.

How does Eiffel handle this?

2) For me, using Cobra 0.8.0, this problem resulted in an unhandled null reference exception. If invariant handling should operate in this fashion, it would seem that this should be handled in a cleaner fashion.

Well the expression ".beverage.cost" in Mocha.cost is the culprit.

What do you think should happen if an invariant expression throws an exception either directly or via the code that it calls into? Right now the exception is raised and then you have to diagnose the problem. I used -d to get the line number of the problem in the stack trace.


-Chuck

[Steve]

1) Should the invariant be called after CondimentDecorator's constructor? It would seem that all invariant checking should be delayed until the end of the original constructor.

That's an interesting question especially with the ancestor classes being abstract. I have to think about it some more.

How does Eiffel handle this?

I think Eiffel would have to apply the invariant once the instance was properly formed (ie; after the Mocha constructor) but I could be wrong. I wish I had 'Eiffel: The Language' or OOSC2 handy so I could double check, but it seems like the original constructor would need to be given the chance to satisfy the invariant clause(s).

2) For me, using Cobra 0.8.0, this problem resulted in an unhandled null reference exception. If invariant handling should operate in this fashion, it would seem that this should be handled in a cleaner fashion.

Well the expression ".beverage.cost" in Mocha.cost is the culprit.

What do you think should happen if an invariant expression throws an exception either directly or via the code that it calls into? Right now the exception is raised and then you have to diagnose the problem. I used -d to get the line number of the problem in the stack trace.

I didn't use the -d. With just the test option, here is what I get:

Testing Mocha...

Unhandled Exception: System.NullReferenceException: Object reference not set to an instance of an object
at Mocha.get_Cost () [0x00000]
at CondimentDecorator.get_Beverage () [0x00000]
at Mocha.get_Cost () [0x00000]
at Beverage..ctor () [0x00000]
at CondimentDecorator..ctor (.Beverage beverage) [0x00000]
at Mocha..ctor (.Beverage beverage) [0x00000]
at Mocha.test_class_Mocha () [0x00000]
at Mocha.RunTests () [0x00000]
at Mocha.RunTestsIfNeeded () [0x00000]
at RunTests.Main () [0x00000]

This definitely lets me know that I had an error, but with just a cursory glance there is nothing to indicate that an invariant was violated. With pre/post conditions, Cobra gives me something like this:

Testing Espresso...

Unhandled Exception: Cobra.Lang.EnsureException:
sourceSite = projects/cobra/Patterns/Decorator/BrokenStarbuzz.cobra:13 in Espresso.cost.get for object Espresso
info = nil
this = Espresso
(result > 0) = false
result = 0 (Decimal)

[Charles]

There's no difference between "invariant" and "require". If the expressions themselves experience an exception, then you will see that exception like so:

class Foo

    get name as String?
        return nil

    def bar as int
        require .name.length > 0
        return 0
    
    def main is shared
        print Foo().bar

# gives:
# Unhandled Exception: System.NullReferenceException: Object reference not set to an instance of an object
#   at Foo.Bar () [0x00000] 
#   at Foo.Main () [0x00000]

The condition never succeeded nor failed, because it never completed. It threw an exception.

And if a condition fails to evaluate to true, then you will get the appropriate exception like so:

class X

    invariant
        .name == 'X'
        
    get name as String
        return 'Y'
    
    def main is shared
        X()
# gives:
# Unhandled Exception: Cobra.Lang.InvariantException: 
# sourceSite = foo-invariant-failed.cobra:4 in X.invariant for object X (MonoType)
# info       = nil
# this       = X (MonoType)
#     (.name == 'X') = false
#     .name = 'Y'
# 
#   at X..ctor () [0x00000] 
#   at X.Main () [0x00000]

Do you feel the exceptions raised by contract conditions should be caught and wrapped up (in RequireException, InvariantException, etc.)?

[Steve]

There's no difference between "invariant" and "require". If the expressions themselves experience an exception, then you will see that exception like so:

class Foo

    get name as String?
        return nil

    def bar as int
        require .name.length > 0
        return 0
    
    def main is shared
        print Foo().bar

# gives:
# Unhandled Exception: System.NullReferenceException: Object reference not set to an instance of an object
#   at Foo.Bar () [0x00000] 
#   at Foo.Main () [0x00000]

The condition never succeeded nor failed, because it never completed. It threw an exception.

And if a condition fails to evaluate to true, then you will get the appropriate exception like so:

class X

    invariant
        .name == 'X'
        
    get name as String
        return 'Y'
    
    def main is shared
        X()
# gives:
# Unhandled Exception: Cobra.Lang.InvariantException: 
# sourceSite = foo-invariant-failed.cobra:4 in X.invariant for object X (MonoType)
# info       = nil
# this       = X (MonoType)
#     (.name == 'X') = false
#     .name = 'Y'
# 
#   at X..ctor () [0x00000] 
#   at X.Main () [0x00000]

Do you feel the exceptions raised by contract conditions should be caught and wrapped up (in RequireException, InvariantException, etc.)?

I see what you are saying, and this does explain the error reported.

I suppose it would be helpful to rethrow these when they occur in contract blocks, at least from a debugging perspective.

Thanks for all your help in this matter,


Steve

--

[Charles]

Has anyone found out how Eiffel handles invariants and base constructors?

The question we have is whether the base constructor should satisfy its own invariant conditions upon completion, or if those should be delayed until the end of the original constructor.

Perhaps we should dig up a free Eiffel compiler or two and try it out.

-Chuck

[Steve]

Has anyone found out how Eiffel handles invariants and base constructors?

The question we have is whether the base constructor should satisfy its own invariant conditions upon completion, or if those should be delayed until the end of the original constructor.

Perhaps we should dig up a free Eiffel compiler or two and try it out.

Actually Chuck, I think I know what the answer would be. Until the constructor for a class has been called, there is no invariant to check, because there is no instance. So if I have Student, which is a descendent of Person and I am trying to instantiate it, the invariant cannot be checked until a fully formed Student has been created.

In the current Cobra implementation, the invariant would be called (if it existed) on class Person, as a Student is manufactured. But this is incorrect on the following grounds:
1) I am not creating a Person. In fact, logically all of the functionality in Student and any parents it has could be flattened, wherein the constructor for Person would just be a routine in Student.
2) Assuming that I did call the invariant in Person, which version do I call? Student's will be more strict - surely this is not correct for building a Person (which we aren't doing anyway), but by the laws of LSP, we can't exactly use the version in Person.

The same applies to preconditions and postconditions. If Child->foo() redefines and calls Parent->foo(), Parent->foo() is not in the business of checking its precondition (a good thing, since this would both be incorrect and incur additional performance penalties). Same goes for the postcondition.

That makes sense, right?


Let me know and best regards as always,


Steve

--

[Charles]

The same applies to preconditions and postconditions. If Child->foo() redefines and calls Parent->foo(), Parent->foo() is not in the business of checking its precondition (a good thing, since this would both be incorrect and incur additional performance penalties). Same goes for the postcondition.

Actually that seems wrong for at least the precondition. An overridden method should check its precondition when invoked via "base.foo" because the code inside is guaranteed to run only if its precondition is met.

Let's say I'm writing a subclass MyList whose superclass is List. I'm overriding the .getAt method:

class List
    def getAt(index as int) as dynamic?
        require index > 0 and index < .count
        return _data[index]

class MyList
    inherits List

    def getAt(index as int) as dynamic? is override
        """
        Accepts any value for index, returning nil if the index is not valid for this list.
        """
        or require true
        if index >= 0 and index <= .count  # bug
            return base.getAt(index)
        else
            return nil

Also, catching errors at the precondition stage makes them easier to diagnose than waiting until a deeper part of the implementation fails (although this trivial example does not make that clear).

I'm not sure why the same wouldn't go for the postcondition. When a subclass says "base.foo" should it not be able to assume that the postcondition of "base.foo" is true at that point?

But constructors/initializers are certainly special beasts, so the issue there is not as clear.

[onodera]

Hello.

I've used the GPL version of EiffelStudio to recreate the cobra code in this topic, and here's what I found:

First, some of the changes I had to do:
CondimentDecorator is no longer abstract/deferred, as abstract classes cannot have constructors in Eiffel.
Description is no longer abstract/deferred in CondimentDecorator as Eiffel forbids redefining defined features as abstract. Instead, it is not overridden there.
Cost in Beverage is no longer an abstract method as it has to be redefined in both Espresso and CondimentDecorator. Instead, it is a query method (no properties in Eiffel) that returns 0.0.

And finally, the results:
The application fails its postcondition (which is the test for Mocha), because Eiffel doesn't use decimal math, but the invariant is not applied until Mocha is created.

[Steve]

The same applies to preconditions and postconditions. If Child->foo() redefines and calls Parent->foo(), Parent->foo() is not in the business of checking its precondition (a good thing, since this would both be incorrect and incur additional performance penalties). Same goes for the postcondition.

Actually that seems wrong for at least the precondition. An overridden method should check its precondition when invoked via "base.foo" because the code inside is guaranteed to run only if its precondition is met.

Let's say I'm writing a subclass MyList whose superclass is List. I'm overriding the .getAt method:

class List
    def getAt(index as int) as dynamic?
        require index > 0 and index < .count
        return _data[index]

class MyList
    inherits List

    def getAt(index as int) as dynamic? is override
        """
        Accepts any value for index, returning nil if the index is not valid for this list.
        """
        or require true
        if index >= 0 and index <= .count  # bug
            return base.getAt(index)
        else
            return nil

Also, catching errors at the precondition stage makes them easier to diagnose than waiting until a deeper part of the implementation fails (although this trivial example does not make that clear).

DbC can be thought of as a contractor/subcontractor relationship, no? So, let's say I've got a contractor to pour concrete for my patio, like so:

class PricySlowContractor
   def pourPatio
      require
         .customerPays == 2000000
      ensure
         .totalTimeSpent == 23 #Days
      body
         ...

PricySlow doesn't really pour the concrete - they instead subcontract it out to CheapFast. This might be like so

class CheapFastContractor
   def pourPatio
      or require
         .customerPays == 2000
      and ensure
         .totalTimeSpent == 1 #Days
      body
         base.pourPatio

Now, the only way that we can satisfy LSP (the central tenant for DbC inheritance) is if we expressly DO NOT check either PricySlow's precondition or postcondition when we tell CheapFast to pour the patio.

I'll double check this (maybe tonight) with SmartEiffel, but this is how I always remember it being. What confuses matters with Eiffel is that in that language, we could both override (Eiffel calls this redefine) and rename PricySlow's version of pourPatio. In the latter case, all of the originals contracts would apply, but in the former, I think that the parent's DbC signature is ignored in favor of the child's so that the examples above comply.