Forums

Invariant Issue

General discussion about Cobra. Releases and general news will also be posted here.
Feel free to ask questions or just say "Hello".

Invariant Issue

Postby Steve » Sun Apr 27, 2008 6:55 am

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

--
Steve
 
Posts: 9

Re: Invariant Issue

Postby Charles » Sun Apr 27, 2008 11:35 am

Steve wrote: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?

Steve wrote: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
Charles
 
Posts: 2515
Location: Los Angeles, CA

Re: Invariant Issue

Postby Steve » Sun Apr 27, 2008 1:24 pm

Chuck wrote:
Steve wrote: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).

Chuck wrote:
Steve wrote: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)
Steve
 
Posts: 9

Re: Invariant Issue

Postby Charles » Sun Apr 27, 2008 4:28 pm

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.)?
Charles
 
Posts: 2515
Location: Los Angeles, CA

Re: Invariant Issue

Postby Steve » Mon Apr 28, 2008 5:43 am

Chuck wrote: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

--
Steve
 
Posts: 9

Re: Invariant Issue

Postby Charles » Fri May 09, 2008 12:43 am

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
Charles
 
Posts: 2515
Location: Los Angeles, CA

Re: Invariant Issue

Postby Steve » Sun May 11, 2008 3:54 pm

Chuck wrote: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

--
Steve
 
Posts: 9

Re: Invariant Issue

Postby Charles » Mon May 12, 2008 2:02 pm

Steve wrote: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.
Charles
 
Posts: 2515
Location: Los Angeles, CA

Re: Invariant Issue

Postby onodera » Tue May 13, 2008 6:20 am

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.
Attachments
cofee.zip
Eiffel code
(2.25 KiB) Downloaded 588 times
onodera
 
Posts: 8

Re: Invariant Issue

Postby Steve » Tue May 13, 2008 11:54 am

Chuck wrote:
Steve wrote: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.
Steve
 
Posts: 9

Next

Return to Discussion

Who is online

Users browsing this forum: No registered users and 6 guests