On Wed, 2 Jan 2013 13:48:07 +0400 MigMit <miguelim...@yandex.ru> wrote: > On Jan 2, 2013, at 10:52 AM, Mike Meyer <m...@mired.org> wrote: > > 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. > Well, you can call that a theory, for sure. But I think it's usually called > an "observation".
An "observation" is what you make to decide if a theory is true or not. In order to make the observation (at least for theories about helping programmers) you need an implementation so you can observe people using it. > I always thought the theory is something that allows us to develop > some new knowledge. Yup. Deciding whether or not the theory is true *is* a development of new knowledge. I can say for a certainty that the documentation aspect of DbC makes me more productive. The testing aspect of it needs more testing (sorry). > Just stating that "comfortable chairs make programmers more > productive" doesn't constitute a theory. Well, it's not very rigorous, and I can think of some counterexamples. On the other hand, if you reparaphrased (sic) it as "Chairs that encourage good posture make programmers more productive", then you have a honest-to-goodness theory. Better yet, it's one that's been thoroughly tested in ergonomics labs around the world. At this point, we're arguing about the semantics of the word "theory". On Wed, 2 Jan 2013 13:41:54 +0400 MigMit <miguelim...@yandex.ru> wrote: > I don't know about DbC in general, but it's implementation in Eiffel > seems to be nothing more than a few ASSERT macros, for some weird > reason embedded into the language. Either you used a particularly poor implementation of Eiffel, or you didn't look at the implementation beyond writing them out. Every Eiffel system I've used included tools that computed the contracts on a method or class (remember, class invariants apply to subclasses, etc.) and displayed them. Those are just as much part of DbC as the "assert macros". If you ignore that usage, you've correctly described things. At least as well as saying that a function call implementation is a goto that records a return address, for some weird reason embedded into the language. Or <higher level construct> is just <implementation method>, for some weird reason embedded into the language. The "weird reason" is pretty much always the same: the construct in question carries more semantic meaning than the implementation method. Functions capture the notion of a distinct, reusable chunk of code, that can have properties all it's own. This is a major step up from just having a goto variant with an otog that undoes it. Likewise, pre and post (and invariant) conditions capture the notion of a contract. They express the terms of the contract implemented by some specific bit of code. The contract is part of the interface to that code. If you're actually doing DbC, it's no less important than the rest of the interface. Like, for instance, the type signature. Personally, I don't believe in turning off the conditions, for much the same reason I don't believe in turning off array bounds checking. I think it's better to get the right answer later than to get the wrong answer now. <mike -- Mike Meyer <m...@mired.org> http://www.mired.org/ Independent Software developer/SCM consultant, email for more information. O< ascii ribbon campaign - stop html mail - www.asciiribbon.org _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe