Re: Static typing, Python, D, DbC

Discussion in 'Python' started by Ed Keith, Sep 12, 2010.

  1. Ed Keith

    Ed Keith Guest

    --- On Sun, 9/12/10, Paul Rubin <> wrote:

    > From: Paul Rubin <>
    > Subject: Re: Static typing, Python, D, DbC
    > To:
    > Date: Sunday, September 12, 2010, 4:28 PM
    > 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.



    Eiffel throws an exception when a contract is violated. That is run time behavior, not static verification.

    -EdK

    Ed Keith


    Blog: edkeith.blogspot.com
     
    Ed Keith, Sep 12, 2010
    #1
    1. Advertising

  2. Ed Keith

    Paul Rubin Guest

    Ed Keith <> writes:
    >> I think DbC as envisioned by the Eiffel guy...
    >> the term is that it's a static verification technique,

    >
    > Eiffel throws an exception when a contract is violated. That is run
    > time behavior, not static verification.


    The runtime checks are for when static analysis hasn't been supplied
    (that is usually a partly manual process). DBC is always intended to be
    statically verified as I understand it. Doing it at runtime is just a
    hackish fallback.
     
    Paul Rubin, Sep 13, 2010
    #2
    1. Advertising

  3. * Paul Rubin, on 13.09.2010 04:50:
    > Ed Keith<> writes:
    >>> I think DbC as envisioned by the Eiffel guy...
    >>> the term is that it's a static verification technique,

    >>
    >> Eiffel throws an exception when a contract is violated. That is run
    >> time behavior, not static verification.

    >
    > The runtime checks are for when static analysis hasn't been supplied
    > (that is usually a partly manual process). DBC is always intended to be
    > statically verified as I understand it. Doing it at runtime is just a
    > hackish fallback.


    DBC can't in generally be statically checked. E.g. a precondition of a routine
    might be that its argument is a sorted array. So regarding the nature of the
    checks it's not hopelessly incompatible with Python.

    Cheers,

    - Alf

    --
    blog at <url: http://alfps.wordpress.com>
     
    Alf P. Steinbach /Usenet, Sep 13, 2010
    #3
  4. Ed Keith

    John Nagle Guest

    On 9/12/2010 7:50 PM, Paul Rubin wrote:
    > Ed Keith<> writes:
    >>> I think DbC as envisioned by the Eiffel guy...
    >>> the term is that it's a static verification technique,

    >>
    >> Eiffel throws an exception when a contract is violated. That is run
    >> time behavior, not static verification.

    >
    > The runtime checks are for when static analysis hasn't been supplied
    > (that is usually a partly manual process). DBC is always intended to be
    > statically verified as I understand it. Doing it at runtime is just a
    > hackish fallback.


    Right.

    Static verification is finally a production technology. 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. That's real "design by contract".

    It's not that relevant to Python, where you can't crash the
    underlying system. But it really matters in languages where you can.

    John Nagle
     
    John Nagle, Sep 13, 2010
    #4
    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:
    582
    Thorsten Ottosen
    Apr 21, 2004
  2. JimLad
    Replies:
    0
    Views:
    523
    JimLad
    Jan 26, 2010
  3. Lie Ryan

    Re: Static typing, Python, D, DbC

    Lie Ryan, Sep 11, 2010, in forum: Python
    Replies:
    7
    Views:
    411
    Paul Rubin
    Sep 13, 2010
  4. Charles Mills

    [ANN] DBC for C 1.1.2

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

Share This Page