Re: Static typing, Python, D, DbC
On 9/12/2010 4:28 PM, Paul Rubin wrote: Bearophilebearophileh...@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
Re: Static typing, Python, D, DbC
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 -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
Bearophile bearophileh...@lycos.com 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. -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
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). -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
John Nagle: Design by contract really isn't a good fit to Python. I have used some times the class invariant done manually, as I have shown, and it has avoided me some bugs, so I have experimentally seen you are wrong. 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. 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. Bye, bearophile -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
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. -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
--- On Sun, 9/12/10, Paul Rubin no.em...@nospam.invalid wrote: From: Paul Rubin no.em...@nospam.invalid Subject: Re: Static typing, Python, D, DbC To: python-list@python.org Date: Sunday, September 12, 2010, 4:28 PM 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. Eiffel throws an exception when a contract is violated. That is run time behavior, not static verification. -EdK Ed Keith e_...@yahoo.com Blog: edkeith.blogspot.com -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
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 -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
Ed Keith e_...@yahoo.com 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. -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
* Paul Rubin, on 13.09.2010 04:50: Ed Keithe_...@yahoo.com 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 -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
On 9/12/2010 7:50 PM, Paul Rubin wrote: Ed Keithe_...@yahoo.com 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 -- http://mail.python.org/mailman/listinfo/python-list
Static typing, Python, D, DbC
I write some Python code almost every day, but lately I am using a lot the D language too. After using D for about three years I now know some of it, but when I need to write short ( about 1000 lines) *correct* programs, Python is still the more productive for me. Static typing, and the usage of transitive const of D are a strange thing. It seems obvious that they lead to safer code, but on the other hand experimentally I have seen that my short Python programs are less buggy than equivalent D ones. Static typing looks safer, but D offers many low level features, and generally it contains many more traps or ways to shoot your own foot, that they more than compensate for the lack of safety coming from Python dynamic typing, even when you don't use those low level features. Maybe for large ( about 100_000 lines) programs D may come out to be less bug-prone than Python (thanks to the better data hiding and static typing), but I am not sure of this at all... Static typing also has a significant costs. When you write D2 code often something doesn't work because of some transitive const or immutable (or just because of the large number of bugs that need to be fixed still in the D compiler). So here you pay some cost as debugging time (or time to avoid those problems). And there is a mental cost too, because you need to keep part of your attention on those const- related things instead of your algorithms, etc. 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: class Foo: def _invariant(self): assert ... assert ... return True def bar(self, ...): assert self._invariant() ... res = ... assert self._invariant() return res But this missed several useful features of DbC. 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. I have installed this, on a Windows Vista OS: http://www.python.org/ftp/python/2.7/python-2.7.msi But I have had two problems, the 'random' module was empty, and it didn't import the new division from the future, so I've had to remove it and reinstall 2.6.6. Is this just a problem of mine? Bye, bearophile -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
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. -- http://mail.python.org/mailman/listinfo/python-list
Re: Static typing, Python, D, DbC
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 -- http://mail.python.org/mailman/listinfo/python-list
