Invariant Issue

[onodera]

I think that redefining honors the contract of the redefined method. That's why it says "and ensure" ("then ensure" in Eiffel). I'll go check it now, just in case.

Edit: Actually, here: http://docs.eiffel.com/eiffelstudio/gen ... al-10.html
Straight from the horse's mouth.
Even if you actually use the CheapFastContractor class, your contract with the PricySlowContractor still holds. It ensures that the work will be done in exactly 23 days and even if your CheapFastContractor can get it done in 1 day, his implementation of the method should include ChewOnAGrassBlade(22) to honor the contract.

[onodera]

And actually, invariants behave the same for constructors and methods.

Code: Select all

class
   ACCOUNT

create
   make

feature

   deposit is
      do
         balance:= 0
      end


   make is
      do
         balance := 0
      end

   balance: INTEGER

invariant
   balance > 0

end

Code: Select all

class
   BETTER_ACCOUNT

inherit
   ACCOUNT
      redefine
         make, deposit
   end

create
   make

feature

   deposit is
      do
         Precursor
         balance := 100
      end

   make is
      do
         Precursor
         balance := 100
      end

end


Code: Select all

class
   APPLICATION

create
   make

feature -- Initialization
   a: BETTER_ACCOUNT
   make is
         -- Run application.
      do

         create a.make
         a.deposit
      end

end -- class APPLICATION

This code runs with no errors. No invariants are checked after a call to the precursor method. Unlike pre- and post-conditions, which are checked when the precursor method is run. Moreover, invariants are checked only after a call from another object. Private calls of any sort do not trigger them.

[Steve]

Even if you actually use the CheapFastContractor class, your contract with the PricySlowContractor still holds. It ensures that the work will be done in exactly 23 days and even if your CheapFastContractor can get it done in 1 day, his implementation of the method should include ChewOnAGrassBlade(22) to honor the contract.

Onodera, Chuck -

I downloaded SmartEiffel last night and checked my assumptions about pre/post conditions and base functionality, and I was definitely mistaken. I haven't programmed in Eiffel now for some 4-5 years, but I had never noted this kind of special consideration when using what Eiffel calls the precursor (base) method.

I guess that the case that I was thinking of was when one would completely rewrite the base version, not relying on the functionality of the original.

From now on though I will definitely run my personal assertions (pun intended ) by the Eiffel compiler before making statements here.

Sorry for the confusion (and good job Onodera!),


Steve

--

[Charles]

No problem. Another way to look at it is to consider that when you have a type of SomeClass, you never know (except in the case of abstract classes) that you'll ever even be dealing with a subclass of SomeClass. It has the be case that you can assert the postconditions of SomeClass.someMethod after invoking it. Otherwise, the contract on .someMethod would be meaningless.

Onodera's comment about not re-invoking contracts when invoking methods on self rang a bell. I missed that in Cobra's implementation and would like for it to match Eiffel's behavior. Would either one of you be interested in enhancing Cobra in this area? I have other things on my plate including patch applications, new print behavior and events, and some parallel effort is always a good thing.

Also, I checked out http://en.wikipedia.org/wiki/SmartEiffel and there was an interesting comment that "In May 2005, after divergences with the working group for the normalization of the Eiffel language, the SmartEiffel project announced that they would not implement the ECMA TC39-TG4 norm." Does anyone know the cause of the divergence? And was the divergence around contracts or other issues?

[onodera]

Onodera's comment about not re-invoking contracts when invoking methods on self rang a bell. I missed that in Cobra's implementation and would like for it to match Eiffel's behavior. Would either one of you be interested in enhancing Cobra in this area? I have other things on my plate including patch applications, new print behavior and events, and some parallel effort is always a good thing.

I'm not sure what is the best way to handle this.
One option is passing an object reference to every method to check for identity before checking invariants. This will break every interface, of course.
Another option is removing invariants from method bodies and adding an additional call after every method invocation that is not dotted or refers to the base class. I don't even want to explain why this won't work.
The final option, which might actually work, is using a stack trace. It might be too slow, though, and I still can't find a way to get to the caller object reference from it.

[Charles]

So one option is creative code generation. Cobra already has some of this with the -detailed-stack-trace option and supporting CobraFrame class.

It appears that the only way to get stack arguments in .NET is to use debugging APIs. There are some links at http://blogs.msdn.com/jmstall/archive/2005/11/08/mdbg_linkfest.aspx

-Chuck

[onodera]

The fourth option I can think of is this:
The invariant code should be added to the method only when it is private/protected.
Every friend/public method should have a private/protected twin that either has a somewhat different name or an extra dummy parameter. Any local/base calls from public/friend methods should call the twin versions.
Every public constructor should likewise have a private twin, but the only option there is having a dummy parameter.