Lambda the Ultimate

inactiveTopic Design By Contract Discussion
started 10/22/2002; 1:55:10 PM - last post 10/24/2002; 12:38:11 PM
Brent Fulgham - Design By Contract Discussion  blueArrow
10/22/2002; 1:55:10 PM (reads: 514, responses: 9)
Eiffel is often treated as the "Red-Headed Stepchild" of the object oriented world. But it has quite a few interesting features that make it worth studying (even in light of the PLT OOPSLA and FSE papers that identify flaws in Eiffel's DbC behavior).

This discussion on the Eiffel newsgroup is quite interesting.

Jarno Virtanen - Re: Design By Contract Discussion  blueArrow
10/22/2002; 9:53:18 PM (reads: 533, responses: 0)
It seems that they fail to mention one very concrete and scientifically sound experiment of the effect of Design by Contract technique, namely a study by Muller, Typke and Hagner named Two controlled Experiments concerning the Usefulness of Assertions as a Means for Programming. (There's also a project page.) They found that DbC increased programming time slightly when developing new code and decreased programming time (slightly, too) in maintenance programming. There was also a little increase in program reliability when using DbC.

In general, I find the studies of that research group interesting. One of their general goals is to test unvalidated hypotheses like that of DbC's effectivity.

Brent Fulgham - Re: Design By Contract Discussion  blueArrow
10/23/2002; 12:43:27 PM (reads: 523, responses: 0)
Jarno -- Thanks very much for this fascinating link! Lots of interesting reading material here.

One thing I would have liked the Muller paper to address was the flaws in the Eiffel DbC dispatching described in the Findler and Felleisen papers. It would be interesting to see if any of the program defects remaining after the code passed the Muller's testing protocol would have been identified using the PLT approach.

For Eiffel proponents, it should be pointed out that Muller's research was done using APP and jContract (not Eiffel). Both of these products are known to suffer from improper dispatch of contracts between parent and child classes (again, see Findler/Felleisen).

Brent Fulgham - Re: Design By Contract Discussion  blueArrow
10/23/2002; 12:47:12 PM (reads: 524, responses: 4)
Another thought -- are you (or others) aware of any research into the equivilency of contract definitions and type?

For example, does a strong contract in effect define the interface to what is effectively a type -- and that contract violations amount to a form of typecast bug?

Ehud Lamm - Re: Design By Contract Discussion  blueArrow
10/23/2002; 1:05:57 PM (reads: 554, responses: 0)
I don't have good reference but the connection is pretty obvious.

Often when you design a type system you want to make type checking (esp. subtype constrinats checked at run time) as efficient as possible. To achieve this you limit the kinds of predicates expressible naturally by the type system. You can then use contracts in cases were the type system is not enough.

I discuss this in my Ada-Europe'2002 paper which applies Findler results to the design of a DbC mechanism for Ada.

A simple example: In Ada you can spcify a range constraint on a Integer subtype.

subtype X is integer range 1..10

If, however, you want to express the predicate "even integer between 1 and 10" you can't do it directly. A contract can help you express this condition.

Note, that you often have ways to hack the type system for you own needs. For example, you can use a type constructor to implement arbitrary checks.

Noel Welsh - Re: Design By Contract Discussion  blueArrow
10/24/2002; 2:56:43 AM (reads: 532, responses: 0)
[Copy of the post below. I guess Manilla doesn't use a continuation based web framework or I wouldn't be able to post the same thing twice.]

Noel Welsh - Re: Design By Contract Discussion  blueArrow
10/24/2002; 2:58:23 AM (reads: 517, responses: 1)
In his talk at ICFP Robby make the point that system defined types often have dynamic checks. E.g. the static type of car is cons but the dynamic type is all cons except the empty list. His contract system allows you to implement these dynamic checks for your own types.

Ehud Lamm - Re: Design By Contract Discussion  blueArrow
10/24/2002; 3:06:35 AM (reads: 546, responses: 0)
This amounts to the same thing I was saying. In Ada, subtype constraints are basically dynamic (i.e., run time), and type checks are at static.

But I think it is useful to stress the notion of expressivness. In order to be efficient type systems are often not as expressive as you'd like them to be.

Brent Fulgham - Re: Design By Contract Discussion  blueArrow
10/24/2002; 12:20:39 PM (reads: 481, responses: 1)
Is the Ada-Europe paper available anyplace as a PDF or PS file? The provided link requires subscription to a service I do not belong to.

Also, did you develop a prototype Ada implementation that can be used with GNAT?

Ehud Lamm - Re: Design By Contract Discussion  blueArrow
10/24/2002; 12:38:11 PM (reads: 507, responses: 0)
I can email you the PDF, next time I am at the office.

I didn't implement the proposed language extension, since I never hacked gnat, and it would have taken me a long time to make additions both to the front end and the back end. Since I was pretty sure nobody is going to support adding DbC to the language at this stage, I didn't really see the point.

As far as hacking gnat goes, I want to implement a call-by-need extension...