Velocity Reviews - Computer Hardware Reviews

Velocity Reviews > Newsgroups > Programming > Python > Re: Static typing, Python, D, DbC

Reply
Thread Tools

Re: Static typing, Python, D, DbC

 
 
Lie Ryan
Guest
Posts: n/a
 
      09-11-2010
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.
 
Reply With Quote
 
 
 
 
John Nagle
Guest
Posts: n/a
 
      09-11-2010
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
 
Reply With Quote
 
 
 
 
Lie Ryan
Guest
Posts: n/a
 
      09-12-2010
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).
 
Reply With Quote
 
Paul Rubin
Guest
Posts: n/a
 
      09-12-2010
Bearophile <(E-Mail Removed)> 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.
 
Reply With Quote
 
Bearophile
Guest
Posts: n/a
 
      09-12-2010
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
 
Reply With Quote
 
Eric S. Johansson
Guest
Posts: n/a
 
      09-13-2010
On 9/12/2010 4:28 PM, Paul Rubin wrote:
> Bearophile<(E-Mail Removed)> 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.Vrie...econdition.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
 
Reply With Quote
 
Bearophile
Guest
Posts: n/a
 
      09-13-2010
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
 
Reply With Quote
 
Paul Rubin
Guest
Posts: n/a
 
      09-13-2010
Bearophile <(E-Mail Removed)> 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.
 
Reply With Quote
 
 
 
Reply

Thread Tools

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off
Trackbacks are On
Pingbacks are On
Refbacks are Off


Similar Threads
Thread Thread Starter Forum Replies Last Post
Re: Static typing, Python, D, DbC Ed Keith Python 3 09-13-2010 04:47 AM
ERROR [HY000] [Microsoft][ODBC Microsoft Access Driver]General error Unable to open registry key 'Temporary (volatile) Jet DSN for process 0xffc Thread 0x228 DBC 0x437b94 Jet'. ERROR [IM006] [Microsoft][ODBC Driver Manager] Driver's SQLSetConnectAttr bazzer ASP .Net 0 03-30-2006 03:16 PM
ERROR [HY000] [Microsoft][ODBC Microsoft Access Driver]General error Unable to open registry key 'Temporary (volatile) Jet DSN for process 0x8fc Thread 0x934 DBC 0x437b94 Jet'. ERROR [IM006] [Microsoft][ODBC Driver Manager] Driver's SQLSetConnectAttr bazzer ASP .Net 1 03-24-2006 04:20 PM
ERROR [HY000] [Microsoft][ODBC Microsoft Access Driver]General error Unable to open registry key 'Temporary (volatile) Jet DSN for process 0x8fc Thread 0x934 DBC 0x437b94 Jet'. ERROR [IM006] [Microsoft][ODBC Driver Manager] Driver's SQLSetConnectAttr bazzer ASP .Net 0 03-24-2006 02:22 PM
Feasability of Design By Contract (DBC) approach in standard C++ christopher diggins C++ 7 04-21-2004 01:20 AM



Advertisments