On 2013-01-02, at 1:52 AM, Mike Meyer <m...@mired.org> wrote: > > > [Context destroyed by top posting.] > MigMit <miguelim...@yandex.ru> wrote: >> But really, "Design by Contract" — a theory? It certainly is a useful >> approach, but it doesn't seem to be a theory, not until we can actually >> prove something about it, and Eiffel doesn't seem to offer anything in >> this direction. > > You just stated (briefly, and not very rigorously) the theory: DbC is a > useful approach to programing. Note that it's a theory about *programming*, > not the resulting program. > >> And by "hack" I meant not the presence of pre/postconditions, but the >> fact that they don't affect anything else. Strip all of them away, and >> you'll have the program which is, essentially, the same (and, in fact, >> pre/postconditions are supposed to be removed in the final version of >> the program). Compare this to Haskell types, for example: an untyped >> version of Haskell won't be able to choose between two class instances, >> so, that would be an entirely different language. > > Type classes are the wrong feature to look at. Type signatures are closer to > what DbC is. Are type signatures a hack to get around deficiencies in the > type inferencing engine? After all, you can strip all of them away and have > essentially the same program.
Eiffel programmers certainly consider the pre&post conditions and invariants to be part of the signature. DbC is closely related to the management of state, and so to the object as a whole not just the parameters to a method. Now, I'm no expert in Haskell so treat the next part of this paragraph accordingly... putting invariants and conditions on monads, in particular to the entry and exit from do notation might be interesting. No particular ideas as to how you'd do that, or even if it'd be useful, but it seems to me to be a bit closer to the level of abstraction where DbC is at in Eiffel. > > Personally, I think the answer is "no", and for the same reason. We add type > signatures to top level functions because it helps document the function, and > to help isolate type errors during compilation. They makes *programming* > easier, even if they don't change the program at all. Pre and Post conditions > (and class invariants - they're also part of DbC!) serve pretty much the same > function. They help document the classes and methods, and tools that generate > class/method documentation from source always include them. They're as > important as the type signature. They also help isolate bugs, in that you get > told explicitly that routine foo passed in an invalid parameter to bar rather > than an exception somewhere deep in the guts of bar that you have to work > back from to find foo. > > As I said before, I'm not sure I agree that the latter is worth the cost of > using them for anything complex. The bugs they uncover are as likely to be in > the pre/post conditions as in the code proper. The documentation benefit is > unquestionable, though. And if some condition is worth documenting, then > having it as executable documentation means it gets tested with the rest of > the code, so you know the documentation is correct. Which means that just > adding conditions to a language misses most of the benefit of DbC. You need > to fix the documentation system as well. I can only speak from personal experience here. I used Eiffel as my primary programming language in the 1990's for about 10 years. I wrote a lot of code in Eiffel, and I used pre&post conditions and class invariants extensively (and loop invariants surprisingly often). Some of that code would certainly be described as 'complex'. Yes, documentation is a huge part of what DbC gives you, but a peculiarly aggressive kind of documentation that tells you when you're doing it wrong. The biggest problem I had with writing pre&post conditions and class invariants was missing part of what should be specified and so letting things pass that shouldn't have. The next biggest problem was being overly specific (I sometimes do the same thing with type signatures in Haskell I'm afraid). Bugs in the code of the conditions and invariants was not much of a problem I found (I can't recall any). It does take a while to learn how to write the conditions and how to accommodate DbC concepts when you write a class or class hierarchy. And, occasionally, the balancing act between DbC and unit tests is tricky. > > This is the kind of theory that you'll find in OOSC: why the features that > are there help make programming easier. Not theories about how they make the > resulting program better. Those two have a lot in common, though. Anything > that makes witing correct code easier generally results in a better program. > -- > Sent from my Android tablet with K-9 Mail. Please excuse my swyping. > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
