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".

Re: Invariant Issue

Postby onodera » Tue May 13, 2008 12:09 pm

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
 
Posts: 8

Re: Invariant Issue

Postby onodera » Tue May 13, 2008 12:59 pm

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.
onodera
 
Posts: 8

Re: Invariant Issue

Postby Steve » Wed May 14, 2008 10:53 am

onodera wrote: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 :D ) by the Eiffel compiler before making statements here.

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


Steve

--
Steve
 
Posts: 9

Re: Invariant Issue

Postby Charles » Thu May 15, 2008 3:20 pm

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

Re: Invariant Issue

Postby onodera » Fri May 16, 2008 9:42 am

Chuck wrote: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.
onodera
 
Posts: 8

Re: Invariant Issue

Postby Charles » Fri May 16, 2008 10:51 am

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

Re: Invariant Issue

Postby onodera » Sat May 17, 2008 2:52 am

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.
onodera
 
Posts: 8

Previous

Return to Discussion

Who is online

Users browsing this forum: No registered users and 11 guests