On 9/12/2010 4:28 PM, Paul Rubin wrote:
Bearophile<bearophileh...@lycos.com> writes:
I see DbC for Python as a way to avoid or fix some of the bugs of the
program, and not to perform proof of correctness of the code. Even if
you can't be certain, you are able reduce the probabilities of some
bugs to happen.
I think DbC as envisioned by the Eiffel guy who coined (and trademarked)
the term is that it's a static verification technique, marketing-speak
annotating subroutines with pre- and post- conditions that can be
checked with Hoare logic. Runtime checks wouldn't qualify as that.
Programming by contract as popularized by Bertrand Meyer (that Eiffel guy) was
designed for run-time checks because that's when errors show. Programming by
contract is based on Dijkstra's weakest precondition work.
http://www.scss.tcd.ie/Edsko.de.Vries/talks/weakest_precondition.pdf
During the last five years before my hands went bad, I spent significant amount
of time working with formal methods and simpler concepts such as design by
contract. Design by contract made the last five years of my programming career
the most rewarding it had ever been. It was nice to finally write code that was
significantly, and measurably better than those coded using Brown 25 (another
fine product from Uranus)[1].
one of the common mistakes have seen about programming by contract or design by
contract is that people assume it's a proof of correctness. It's not, it's an
experiential proof that the code is executing correctly to the extent that
you've characterized the pre-and post-conditions. Formal proofs are considered a
dead-end as far as I can tell but it's been a good number of years since I've
really investigated that particular domain.
If my opinion is worth anything to anyone, I would highly recommend adopting
some form of programming by contract in everything you write. use the
properties that Dijkstra taught us with the weakest precondition to test only
what you need to test. If you are careless, assertions can build up to a
significant percentage of the code base and Slow execution. the argument for
dealing with this, last time I looked, was that you turn off assertions when
your code is "running". This logic is flawed because bugs exist and will assert
themselves at the worst possible time which usually means after you turned off
the assertions. Personally, I see assertions as another form of defensive
programming. If you can define preconditions as excluding bad data, then your
mainline body becomes faster/smaller.
Anyway, this debate was going on circa 1990 and possibly even earlier when
Dykstra wrote his first papers. Consider me a double plus vote for strong
programming by contract capability in Python. If I can ever get programming by
voice working in a reasonable way, I might even be able to use it. :-)
PS, to explain Brown 25 in case you weren't watching "those damn kids" comedy
movies in the 1970s with a bunch of very stoned friends. Thank God for campus
buses keeping us out of cars.
[1] http://www.youtube.com/watch?v=008BPUdQ1XA
--
http://mail.python.org/mailman/listinfo/python-list
