Re: Static typing, Python, D, DbC

Discussion in 'Python' started by Lie Ryan, Sep 11, 2010.

  1. Lie Ryan

    Lie Ryan Guest

    On 09/12/10 00:33, Bearophile wrote:

    > ----------------
    >
    > Lately while I program with Python one of the D features that I most
    > miss is a built-in Design By Contract (see PEP 316), because it avoids
    > (or helps me to quickly find and fix) many bugs. In my opinion DbC is
    > also very good used with doctests.


    > You may implement a poor's man DbC in Python like this:


    I would do it like this:

    from DbC import DbC
    class Foo(__metaclass__=DbC):
    def __invariant(self):
    ... automatically asserted for all methods ...
    def __precond(self):
    ... automatically asserted for all methods ...
    def __postcond(self):
    ... automatically asserted for all methods ...

    @precond(attr=value) # asserts self.attr==value
    @postcond(func) # a function for more complex assertions
    def bar(self, ...):
    ... clean, uncluttered code ...

    and set DbC.uninstall() to uninstall all precond/postcond/invariants at
    runtime without any additional overhead. These are all definitely
    possible with metaclasses and decorators.

    > From the D standard library, I have also appreciated a lazy string
    > split (something like a str.xplit()). In some situations it reduces
    > memory waste and increases code performance.


    Care to open an issue at the tracker? Considering that many Python 3
    builtins is now lazy, there might be a chance this is an oversight, or
    there might be a reason why string.split is not lazy.
    Lie Ryan, Sep 11, 2010
    #1
    1. Advertising

  2. Lie Ryan

    John Nagle Guest

    On 9/11/2010 9:36 AM, Lie Ryan wrote:
    > On 09/12/10 00:33, Bearophile wrote:
    >
    >> ----------------
    >>
    >> Lately while I program with Python one of the D features that I most
    >> miss is a built-in Design By Contract (see PEP 316), because it avoids
    >> (or helps me to quickly find and fix) many bugs. In my opinion DbC is
    >> also very good used with doctests.

    >
    >> You may implement a poor's man DbC in Python like this:

    >
    > I would do it like this:


    Design by contract really isn't a good fit to Python. I've
    done proof of correctness work, and there are suitable languages
    for it. It needs a language where global static analysis is
    possible, so you can reliably tell what can changes what.

    John Nagle
    John Nagle, Sep 11, 2010
    #2
    1. Advertising

  3. Lie Ryan

    Lie Ryan Guest

    On 09/12/10 08:53, John Nagle wrote:
    > On 9/11/2010 9:36 AM, Lie Ryan wrote:
    >> On 09/12/10 00:33, Bearophile wrote:
    >>
    >>> ----------------
    >>>
    >>> Lately while I program with Python one of the D features that I most
    >>> miss is a built-in Design By Contract (see PEP 316), because it avoids
    >>> (or helps me to quickly find and fix) many bugs. In my opinion DbC is
    >>> also very good used with doctests.

    >>
    >>> You may implement a poor's man DbC in Python like this:

    >>
    >> I would do it like this:

    >
    > Design by contract really isn't a good fit to Python. I've
    > done proof of correctness work, and there are suitable languages
    > for it. It needs a language where global static analysis is
    > possible, so you can reliably tell what can changes what.


    As long as you're not using some funny magic (e.g. monkey patching);
    then IMO python copes reasonably well. Though, I agree, Python probably
    isn't really suitable for formal proofing (the best way to assert
    program's correctness in python is by unittesting, which isn't a formal
    proof, just one that works most of the time).
    Lie Ryan, Sep 12, 2010
    #3
  4. Lie Ryan

    Paul Rubin Guest

    Bearophile <> 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.
    Paul Rubin, Sep 12, 2010
    #4
  5. Lie Ryan

    Bearophile Guest

    Paul Rubin:
    > 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.


    The implementations of DbC in D and C# run their tests at run-time
    (but in theory an external tool may find a way to perform part of
    those tests at compile-time).

    A full implementation of DbC contains several other things beside
    preconditions and postconditions, see http://www.python.org/dev/peps/pep-0316/
    (it misses few things like loop invariants and loop variants).

    For me DbC is useful almost as unit-testing (I use them at the same
    time), this is why in the original post I have said it's one of the
    things I miss most in Python.

    Bye,
    bearophile
    Bearophile, Sep 13, 2010
    #5
  6. On 9/12/2010 4:28 PM, Paul Rubin wrote:
    > Bearophile<> 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
    Eric S. Johansson, Sep 13, 2010
    #6
  7. Lie Ryan

    Bearophile Guest

    John Nagle:

    > All signed Windows 7 drivers must pass Microsoft's static checker,
    > which checks that they don't have bad pointers and call all the
    > driver APIs correctly.


    I didn't know this, thank you. I'll read more about this topic.

    ----------------

    Eric S. Johansson:

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


    These are real problems.

    In some situations the code is "fast enough" even with those runtime
    tests, so in those situations it's better to keep them active even in
    release builds or when you use the program (this is often true for
    small script-like programs).

    But in some situations you want a faster final program. Running the
    run-time contracts only when you test the code and removing them when
    you run the program for real sounds silly or dangerous. But life is
    made of trade-offs, and running those contracts during testing is
    better than _never_ running them. In practice if your tests are done
    well enough (they are similar to the real usage of the program), the
    contracts are able to catch most of the bugs anyway before the release
    build.

    The run-time contracts may slow down the code, but there are few ways
    to reduce this problem. You have to write your contracts taking care
    of not changing the computational complexity of the routine/method
    they guard (so you usually don't want to perform a O(n) test for a
    routine with O(n ln n) worst-case complexity).

    You run your tests often, so if some tests are too much slow you see
    it soon and you may fix the problem (the same is true for slow unit
    tests).

    In D there are several ways to "layer" the work you perform at
    runtime, there is not just the release build and test build. You have
    the version and debug statements, you may use them inside DbC
    contracts too. So in normal test builds I use faster contracts, but if
    I spot a bug I lower the debug level and I recompile the D code,
    activating heavier tests, to better spot where the bug is. One good
    thing of DbC is that when the "density" of presence of contracts in
    your programs gets higher of some threshold, most of the bugs present
    in the code show themselves up as failed assertions/contracts. To me
    it seems related to percolation theory :) (http://en.wikipedia.org/
    wiki/Percolation_threshold ).

    In D you may also use enforce(), that's essentially a camouflaged
    throw/raise statement, if you use it outside DbC contracts, they are
    tests that run even in release builds when your contracts are
    disabled.

    Bye,
    bearophile
    Bearophile, Sep 13, 2010
    #7
  8. Lie Ryan

    Paul Rubin Guest

    Bearophile <> writes:
    > But in some situations you want a faster final program. Running the
    > run-time contracts only when you test the code and removing them when
    > you run the program for real sounds silly or dangerous. But life is
    > made of trade-offs, and running those contracts during testing is
    > better than _never_ running them.


    For some programs, having the contracts fail during running "for real"
    is intolerable, so if you're not ready to remove the runtime tests, then
    program is not ready to run for real.

    The Wikipedia article about DBC

    http://en.wikipedia.org/wiki/Design_by_contract

    makes it sound like what I thought, the preferred enforcement method is
    static, but runtime testing can be used as a fallback. I'm pretty sure
    Eiffel itself comes with static DBC tools.
    Paul Rubin, Sep 13, 2010
    #8
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. christopher diggins
    Replies:
    7
    Views:
    552
    Thorsten Ottosen
    Apr 21, 2004
  2. JimLad
    Replies:
    0
    Views:
    489
    JimLad
    Jan 26, 2010
  3. Ed Keith

    Re: Static typing, Python, D, DbC

    Ed Keith, Sep 12, 2010, in forum: Python
    Replies:
    3
    Views:
    297
    John Nagle
    Sep 13, 2010
  4. Charles Mills

    [ANN] DBC for C 1.1.2

    Charles Mills, Nov 2, 2004, in forum: Ruby
    Replies:
    0
    Views:
    85
    Charles Mills
    Nov 2, 2004
  5. Charles Oliver Nutter
    Replies:
    4
    Views:
    132
    Rick DeNatale
    Oct 2, 2007
Loading...

Share This Page