status of Programming by Contract (PEP 316)?

On Aug 29, 7:21 am, Russ <uymqlp...@sneakemail.comwrote:

>
Thanks for that information. That's too bad, because it seems like a
strong positive capability to add to Python. I wonder why the cold
reception. Were there problems with the idea itself or just the
implementation? Or is it just a low priority?

Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.

In any case, I guess it is still perfectly usable even if it isn't
part of the core Python. Has anyone used it? If so, how well did it
work? Thanks.

Dunno, I would be curious myself to know if there are users
of these frameworks (including AOP frameworks in Python) or
if they are just exercises.

Michele Simionato

Aug 29 '07 #4

Russ

On Aug 28, 10:58 pm, Michele Simionato <michele.simion...@gmail.com>
wrote:

Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.

I get the strong impression you don't really understand what
programming by contract is.

I have not yet personally used it, but I am interested in anything
that can help to make my programs more reliable. If you are
programming something that doesn't really need to be correct, than you
probably don't need it. But if you really need (or want) your software
to be correct and reliable as possible, I think you you should be
interested in it. You might want to read this:

http://archive.eiffel.com/doc/manual...iane/page.html

Aug 29 '07 #5

On Aug 29, 8:45 am, Russ <uymqlp...@sneakemail.comwrote:

I get the strong impression you don't really understand what
programming by contract is.

I have not yet personally used it, but I am interested in anything
that can help to make my programs more reliable. If you are
programming something that doesn't really need to be correct, than you
probably don't need it. But if you really need (or want) your software
to be correct and reliable as possible, I think you you should be
interested in it. You might want to read this:

http://archive.eiffel.com/doc/manual...ct/ariane/page...

That paper contains only a good think: a link to the contrarian view
http://home.flash.net/~kennieg/ariane.html#s3.1.5

Aug 29 '07 #6

Aahz

In article <11**********************@z24g2000prh.googlegroups .com>,
Russ <uy*******@sneakemail.comwrote:

>
I just stumbled onto PEP 316: Programming by Contract for Python
(http://www.python.org/dev/peps/pep-0316/). This would be a great
addition to Python, but I see that it was submitted way back in 2003,
and its status is "deferred." I did a quick search on comp.lang.python,
but I don't seem to see much on it. Does anyone know what the real
status is of getting this into standard Python? Thanks.

The way to get this into Python is to get people to use it as a
stand-alone module. It's already in PyPI, so now it's time for some
marketing.
--
Aahz (aa**@pythoncraft.com) <* http://www.pythoncraft.com/

"If you don't know what your program is supposed to do, you'd better not
start writing it." --Dijkstra

Aug 29 '07 #7

Dan Stromberg - Datallegro

On Tue, 28 Aug 2007 23:45:28 -0700, Russ wrote:

On Aug 28, 10:58 pm, Michele Simionato <michele.simion...@gmail.com>
wrote:

>Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.

I get the strong impression you don't really understand what
programming by contract is.

I have not yet personally used it, but I am interested in anything
that can help to make my programs more reliable. If you are
programming something that doesn't really need to be correct, than you
probably don't need it. But if you really need (or want) your software
to be correct and reliable as possible, I think you you should be
interested in it. You might want to read this:

http://archive.eiffel.com/doc/manual...iane/page.html

I agree with Chris - there's no need to be condescending.

However, I agree with you that this is a valuable addition to a language.

It's not that Eiffel, by having preconditions and postconditions, is doing
anything that cannot be done in python already.

It's more that by making these things a formal part of the language, or at
least a module that facilitates them, one gives a sort of stamp of
approval to adding a ton of assertions about how your code is supposed to
work /when/working/in/that/language, which makes debugging a relative
snap. Isn't that something people should want for python? Sturdy code
and easy debugging?

I've been trying to write my python code with tons of "unnecessary" if
statements that check out my assumptions, and I'm finding more or less
what the Eiffel people claim: I'm investing a little bit of upfront time,
and getting a huge payoff in the backend as my code starts to debug
itself. But I likely never would've started taking my error checking to
such extremes if I hadn't been curious about Eiffel for a while.

Throwing in tons of error and assumption checking mostly eliminates silly
tracing from procedure to function to procedure to function, trying to
find the ultimate root cause of a problem. Usually, the root cause is
identified in an error on stderr or similar.

Keep in mind that debugging usually takes far longer than the initial
coding. Programming by contract seems to balance that out, relatively
speaking.

Granted, we could just say "You should check for these things anyway", or
"You should know what you're doing", but... Isn't that kind of what
assembler programmers used to say to Lisp, FORTRAN and COBOL programmers?

And what about the case where you've written a piece of code, and
someone else has written another, and the two pieces of code need to
interact? Odds are pretty good that if this code has much substance,
there'll be opportunity for subtly different assumptions about what should
be happening in each (yes, "well abstracted" code will be
misassumption-resistant, but even the best OOP programmers will run afoul
of this /sometimes/). Perhaps both these programmers "Know what they're
doing", but they don't necessarily know what the other is doing!

IMO, putting Programming by Contract into python as part of the language
itself, or as a simple module, is a little bit like a company or
department coming up with a mission statement. It's easy to say that it's
meaningless, and some will ignore it, but it still kind of sets the tone
for how things "should be done".

Aug 29 '07 #8

Russ

But it's always a good idea to make your software "correct and as
reliable as possible", isn't it? The problem is the external constraints
on the project. As the old saying goes: "Cheap, fast, reliable: choose
any two".

If you are suggesting that "programming by contract" is not
appropriate for every application, you will get no argument from me.
All I am suggesting is that having the option to use it when you need
it is very desirable, and it can possibly enhance the versatility of
Python by making Python more suitable for *some* mission-critical
applications.

I once read a book on something called SPARK Ada, which also supports
programming by contract. I was pleasantly surprised to discover
yesterday that support for the such methods is also available for
Python. However, the support would obviously be a bit stronger if it
were in the core Python distribution.

What I really like about the implementation I cited above is that the
invariants and the pre and post-conditions can all be put right in the
doc string at the beginning of each class or function. You can think
of it as a detailed specification of the intent (or of some of the
requirements or constraints) of the class or function -- which can be
*automatically* checked during testing. It can also be used for
explicit type checking.

It's like having some of your most critical unit tests built right
into your code. It may make your code very verbose, but it will also
be very complete.

Aug 29 '07 #9

On Aug 30, 1:17 am, Dan Stromberg - Datallegro
<dstromb...@datallegro.comwrote:

IMO, putting Programming by Contract into python as part of the language
itself, or as a simple module, is a little bit like a company or
department coming up with a mission statement. It's easy to say that it's
meaningless, and some will ignore it, but it still kind of sets the tone
for how things "should be done".

I disagree. IMO automatic testing is thousands of times better than
design by contract and Python has already all the support you need
(unittest, doctest, py.test, nose, ...)
Michele Simionato

Aug 30 '07 #10

Chris Mellon

On 8/29/07, Russ <uy*******@sneakemail.comwrote:

>
But it's always a good idea to make your software "correct and as
reliable as possible", isn't it? The problem is the external constraints
on the project. As the old saying goes: "Cheap, fast, reliable: choose
any two".

If you are suggesting that "programming by contract" is not
appropriate for every application, you will get no argument from me.
All I am suggesting is that having the option to use it when you need
it is very desirable, and it can possibly enhance the versatility of
Python by making Python more suitable for *some* mission-critical
applications.

PEP 316 introduces new syntax for a limited use feature. That's pretty
much a no-starter, in my opinion, and past experience tends to bear
that out. Furthermore, it predates decorators and context managers,
which give all the syntax support you need and let you move the actual
DBC features into a library. I can't remember if I mentioned this
before but I believe that Philip Ebys PEAK toolkit has some stuff you
could use for DBC.

I once read a book on something called SPARK Ada, which also supports
programming by contract. I was pleasantly surprised to discover
yesterday that support for the such methods is also available for
Python. However, the support would obviously be a bit stronger if it
were in the core Python distribution.

If a well written contract library were to exist, and people were to
use it, and the author were interested, it would make a decent
candidate for inclusion in the standard library, and I wouldn't oppose
such a thing (for all my opinion is worth, ie essentially nothing).
The PEP 316 special syntax is another matter entirely.

The best way for this to happen is for you to find or write such a
library, and use it to write good code.

Aug 30 '07 #11

Russ

PEP 316 introduces new syntax for a limited use feature. That's pretty
much a no-starter, in my opinion, and past experience tends to bear
that out. Furthermore, it predates decorators and context managers,
which give all the syntax support you need and let you move the actual
DBC features into a library. I can't remember if I mentioned this
before but I believe that Philip Ebys PEAK toolkit has some stuff you
could use for DBC.

I don't see how you can avoid adding some new syntax, given that
Python does not
currently have syntax for specifying invariants and pre- and post-
conditions. And if I am
not mistaken, the new syntax would appear only in doc strings, not in
the regular Python
code itself. We're not really talking here about changing the core
Python syntax itself,
so I don't see it as a "non-starter." Anyone who chooses not to use
would be completely
unaffected.

As far as I can tell, Terence Way has done a nice job of implementing
design by contract for
Python, but perhaps a better approach is possible. The advantage of
making part of the
core Python distribution is that it would get vetted more thoroughly.

Aug 30 '07 #12

Chris Mellon

On 8/30/07, Russ <uy*******@sneakemail.comwrote:

>
PEP 316 introduces new syntax for a limited use feature. That's pretty
much a no-starter, in my opinion, and past experience tends to bear
that out. Furthermore, it predates decorators and context managers,
which give all the syntax support you need and let you move the actual
DBC features into a library. I can't remember if I mentioned this
before but I believe that Philip Ebys PEAK toolkit has some stuff you
could use for DBC.

I don't see how you can avoid adding some new syntax, given that
Python does not
currently have syntax for specifying invariants and pre- and post-
conditions. And if I am
not mistaken, the new syntax would appear only in doc strings, not in
the regular Python
code itself. We're not really talking here about changing the core
Python syntax itself,
so I don't see it as a "non-starter." Anyone who chooses not to use
would be completely
unaffected.

I misread the pep as adding the identifiers into the actual python
syntax, not in the docstring. All the more reason to implement it as a
library, then. I actually think that decorators and context managers
would be nicer than special docstring syntax, but I recognize the
benefit of the doctest style approach.

As far as I can tell, Terence Way has done a nice job of implementing
design by contract for
Python, but perhaps a better approach is possible. The advantage of
making part of the
core Python distribution is that it would get vetted more thoroughly.

Things get vetted *before* they get added to the core, not after.

Aug 30 '07 #13

Russ

Things get vetted *before* they get added to the core, not after.

I realize that. I meant that it would get vetted in the process of
putting it into the core. That
would provide more confidence that it was done the best possible way
-- or close to it.

Aug 30 '07 #14

Russ a écrit :
(snip)

I don't see how you can avoid adding some new syntax, given that
Python does not
currently have syntax for specifying invariants and pre- and post-
conditions.

class Parrot(object):
@pre(lambda x : x != 42)
@post(lambda result: result != 42)
@invariant(lambda self: self.x == 42)
def reliable_method(self, x):
# your code here
return something

Aug 30 '07 #15

Russ a écrit :

On Aug 28, 10:58 pm, Michele Simionato <michele.simion...@gmail.com>
wrote:

>>Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.

I get the strong impression you don't really understand what
programming by contract is.

I get the strong impression you don't really understand how
condescending you are.

I have not yet personally used it,

You have no working experience with the concept, but you think it should
make it into Python's core ???

Aug 30 '07 #16

Russ

Bruno Desthuilliers wrote:

Russ a écrit :
(snip)

I don't see how you can avoid adding some new syntax, given that
Python does not
currently have syntax for specifying invariants and pre- and post-
conditions.

class Parrot(object):
@pre(lambda x : x != 42)
@post(lambda result: result != 42)
@invariant(lambda self: self.x == 42)
def reliable_method(self, x):
# your code here
return something

That looks like new syntax to me. Did I miss your point?

I have no strong leaning about what the exact syntax should be for
programming by contract.
The syntax you show above seems reasonable, except that I am not sure
about requiring
that everything be put inside parentheses. That seems a bit confining
for more complex
conditions.

Aug 30 '07 #17

Chris Mellon

On 8/30/07, Russ <uy*******@sneakemail.comwrote:

>
Bruno Desthuilliers wrote:
Russ a écrit :
(snip)

I don't see how you can avoid adding some new syntax, given that
Python does not
currently have syntax for specifying invariants and pre- and post-
conditions.
class Parrot(object):
@pre(lambda x : x != 42)
@post(lambda result: result != 42)
@invariant(lambda self: self.x == 42)
def reliable_method(self, x):
# your code here
return something

That looks like new syntax to me. Did I miss your point?

I have no strong leaning about what the exact syntax should be for
programming by contract.
The syntax you show above seems reasonable, except that I am not sure
about requiring
that everything be put inside parentheses. That seems a bit confining
for more complex
conditions.

This is existing, working python syntax (although the decorators would
need to be defined).

--
http://mail.python.org/mailman/listinfo/python-list

Aug 30 '07 #18

Russ

Bruno Desthuilliers wrote:

Russ a écrit :
On Aug 28, 10:58 pm, Michele Simionato <michele.simion...@gmail.com>
wrote:

>Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.

I get the strong impression you don't really understand what
programming by contract is.

I get the strong impression you don't really understand how
condescending you are.

When someone writes something as ignorant as that, they need to be
called on it.

So you can implement everything you need already in Python? Yes, of
course, and you
can do it in machine language too -- if you have the time to waste.

I have not yet personally used it,

You have no working experience with the concept, but you think it should
make it into Python's core ???

I don't need to use it to understand the concept. That has been
explained
brilliantly by the Eiffel and SPARK Ada folks.

I am also smart enough to figure out that
it can greatly enhance unit testing, and it can also be used as an
integral part of unit testing.
Once you have the conditions in place, all you need to do in your unit
tests is to send inputs
to the unit and wait to see if exceptions are thrown.

In fact, I would even propose a new name for "programming by
contract." I would call it
"self-testing code" because the code essentially tests itself every
time it is run with the
checks activated.

Aug 30 '07 #19

Russ a écrit :

Bruno Desthuilliers wrote:

>>Russ a écrit :
(snip)

>>>I don't see how you can avoid adding some new syntax, given that
Python does not
currently have syntax for specifying invariants and pre- and post-
conditions.

class Parrot(object):
@pre(lambda x : x != 42)
@post(lambda result: result != 42)
@invariant(lambda self: self.x == 42)
def reliable_method(self, x):
# your code here
return something

That looks like new syntax to me.

It's the syntax for decorator functions, and it's not that new - it
cames with Python 2.4, released November 30, 2004.

Did I miss your point?

Yes.

Aug 31 '07 #20

Ryan Ginstrom

On Behalf Of Russ

Once you have the conditions in place, all you need to do in
your unit tests is to send inputs to the unit and wait to see
if exceptions are thrown.

That sounds a little ambitious to me...

However, you may want to look at the typecheck module (you can get it via
easy_install). I think you could probably extend it to do DBC.
http://oakwinter.com/code/typecheck/

>>from typecheck import accepts, returns, Any
@accepts(str, int, Any())

@returns(list)
def makelist(a, b, c):
return [a, b, c]

>>makelist("spam", 42, object())

['spam', 42, <object object at 0x00AE0470>]

>>makelist(42, "spam", 3.4)

Traceback (most recent call last):
File "<pyshell#25>", line 1, in <module>
makelist(42, "spam", 3.4)
File
"C:\Python25\lib\site-packages\typecheck-0.3.5-py2.5.egg\typecheck\__init__.
py", line 1340, in fake_function
File
"C:\Python25\lib\site-packages\typecheck-0.3.5-py2.5.egg\typecheck\__init__.
py", line 1419, in __check_args
TypeCheckError: Argument a: for 42, expected <type 'str'>, got <type 'int'>

>>>

I tried using DBC for a time in C++ (using a library with a clever
assembly-language hack). I personally found it neater having such code in
unit tests, but obviously, it's a matter of preference.

Regards,
Ryan Ginstrom

Aug 31 '07 #21

Russ

That looks like new syntax to me.

It's the syntax for decorator functions, and it's not that new - it
cames with Python 2.4, released November 30, 2004.

After looking more carefully at your example, I don't think it is as
clean and logical as the
PEP 316 syntax. At first I thought that your pre and post-conditions
applied to the class,
but now I realize that they apply to the function. I prefer to see the
conditions inside
the function in the doc string. That just seems more logical to me.
With all due respect,
your proposal is interesting, but I think it overextends the "function
decorator" idea a bit.

A nit-pick I might have with the PEP 316 syntax is that I think
"invariant" should be spelled
out rather than abbreviated as "inv". The same might apply to "pre-
condition" and
"post-condition". But that's obviously no big deal.

Aug 31 '07 #22

Russ a écrit :

Bruno Desthuilliers wrote:

>>Russ a écrit :

>>>On Aug 28, 10:58 pm, Michele Simionato <michele.simion...@gmail.com>
wrote:

Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.
I get the strong impression you don't really understand what
programming by contract is.

I get the strong impression you don't really understand how
condescending you are.

When someone writes something as ignorant as that, they need to be
called on it.

When someone writes something as arrogant as that, they need to be
called on it.

Michele obviously knows what DbC is (probably better than you do), and
he also knows Python enough to know why you don't need to add anything
to Python to have it.

So you can implement everything you need already in Python?

Talking about DbC ?

Yes, of
course,

"Yes, of course". A couple of decorator functions and you're done. It's
pretty trivial, and that's why Michele told you could implement it by
yourself.

(snip)

>>>I have not yet personally used it,

You have no working experience with the concept, but you think it should
make it into Python's core ???

I don't need to use it to understand the concept. That has been
explained
brilliantly by the Eiffel and SPARK Ada folks.

FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained" why
one can not hope to "write reliable programs" without strict static
declarative type-checking.

One needs to have working experience with a concept to know what it's
really worth. Too bad for you, you're too "smart" to understand this.

I am also smart enough

Yes, obviously really smart.

Aug 31 '07 #23

Russ a écrit :

>>>That looks like new syntax to me.

It's the syntax for decorator functions, and it's not that new - it
cames with Python 2.4, released November 30, 2004.

After looking more carefully at your example, I don't think it is as
clean and logical as the
PEP 316 syntax.

Possibly not, but at least it's trivial to implement.

At first I thought that your pre and post-conditions
applied to the class,

Pre and post conditions applying to the class ? Now that's an
interesting concept. IIRC, Eiffels pre and post conditions only apply to
methods, and I fail to see how they could apply to a class. But since
you're an expert on the subject, I don't doubt you'll enlighten us ?

but now I realize that they apply to the function. I prefer to see the
conditions inside
the function in the doc string. That just seems more logical to me.

Not to me. Doc strings are not for implementation. But if you want to
implement a DbC module using doc strings, please do so.

With all due respect,
your proposal is interesting, but I think it overextends the "function
decorator" idea a bit.

Definitively not, on the contrary - that's *exactly* what decorators are
for. Else, they would be nothing more than HOFs, and there would be no
point in having this syntactic sugar.

(snip).

Aug 31 '07 #24

Russ

Ryan Ginstrom wrote:

I tried using DBC for a time in C++ (using a library with a clever
assembly-language hack). I personally found it neater having such code in
unit tests, but obviously, it's a matter of preference.

I agree that it ultimately boils down to preference, but as I tried to
explain earlier, I don't
think that unit tests are equivalent to DBC (or, as I referred to it
earlier, "self-testing code").

Unit tests are not automatically executed when you run your
application. You need to write
the drivers and generate sample inputs to all the functions in your
application, which
can be very time-consuming. And if you think you can anticipate all
the weird internal data
that might come up in the execution of your application, then either
your application is very
simple or you are fooling yourself.

With self-testing code, on the other hand, all you need to do is to
get sample inputs to
your application (not internal inputs to functions) and run the entire
application. That is
much simpler and more comprehensive than unit testing.

Again, I recognize that it doesn't necessarily replace unit testing
completely. For one thing,
unit testing can test for specific outputs for specific inputs,
whereas you wouldn't want to
clutter your actual code with such specific cases. For example, a unit
test for a sorting
function could provide a specific input and test for a specific
output, but you probably
wouldn't want to clutter your code with such a case. The self-tests in
your code would be
more for general tests. PEP 316 provides an excellent of comprehensive
tests for a sorting
function. If you pass those tests, you can be sure your function
worked correctly.

Aug 31 '07 #25

Russ

Pre and post conditions applying to the class ? Now that's an
interesting concept. IIRC, Eiffels pre and post conditions only apply to
methods, and I fail to see how they could apply to a class. But since
you're an expert on the subject, I don't doubt you'll enlighten us ?

I made a simple mistake. Excuse me. Oh wait ... aren't you one of the
sensitivity police who
laid into me for criticizing someone else. For the record, the guy I
criticized
made ridiculous assertions about DBC. All I did was to make a simple
mistake about
an inconsequential matter. No, pre and post conditions obviously don't
apply to classes,
but all I said was that that's how it appeared to me "at first
glance."

If you are upset about my criticism of one of your colleagues, please
tell him to quite making
outrageous assertions about something he obviously knows little about.

Aug 31 '07 #26

Russ

FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained" why
one can not hope to "write reliable programs" without strict static
declarative type-checking.

And they are probably right.

I don't think you understand what they mean by "reliable
programs." Any idea how much Python is used for flight control systems
in commercial
transport aircraft or jet fighters? How about ballistic missile launch
and guidance systems?
Any idea why?

For the record, I think that DBS could possibly make Python more
suitable for *some*
mission-critical or perhaps even safety-critical applications, but it
will never be able
to compete with SPARK Ada or even Ada at the highest level of that
domain.

The important question is this: why do I waste my time with bozos like
you?

Aug 31 '07 #27

Bruno Desthuilliers <bd*****************@free.quelquepart.frwrites:

FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained"
why one can not hope to "write reliable programs" without strict
static declarative type-checking.

I don't know about Eiffel but at least an important subset of SPARK
Ada's DBC stuff is done using static analysis tools (not actually
built into the compiler as it happens) to verify statically
(i.e. without actually running the code) that the code fulfills the
DBC conditions. I don't see any way to do that with Python
decorators.

Aug 31 '07 #28

Russ

Paul Rubin wrote:

Bruno Desthuilliers <bd*****************@free.quelquepart.frwrites:
FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained"
why one can not hope to "write reliable programs" without strict
static declarative type-checking.

I don't know about Eiffel but at least an important subset of SPARK
Ada's DBC stuff is done using static analysis tools (not actually
built into the compiler as it happens) to verify statically
(i.e. without actually running the code) that the code fulfills the
DBC conditions. I don't see any way to do that with Python
decorators.

Yes, thanks for reminding me about that. With SPARK Ada, it is
possible for some real
(non-trivial) applications to formally (i.e., mathematically) *prove*
correctness by static
analysis. I doubt that is possible without "static declarative type-
checking."

SPARK Ada is for applications that really *must* be correct or people
could die. With all
due respect, most (not all, but most) Python programmers never get
near such programs
and have no idea about how stringent the requirements are. Nor do most
programmers
in general, for that matter. (It's not an insult)

Aug 31 '07 #29

=?ISO-8859-1?Q?Ricardo_Ar=E1oz?=

Russ wrote:

Paul Rubin wrote:
>Bruno Desthuilliers <bd*****************@free.quelquepart.frwrites:
>>FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained"
why one can not hope to "write reliable programs" without strict
static declarative type-checking.
I don't know about Eiffel but at least an important subset of SPARK
Ada's DBC stuff is done using static analysis tools (not actually
built into the compiler as it happens) to verify statically
(i.e. without actually running the code) that the code fulfills the
DBC conditions. I don't see any way to do that with Python
decorators.

Yes, thanks for reminding me about that. With SPARK Ada, it is
possible for some real
(non-trivial) applications to formally (i.e., mathematically) *prove*
correctness by static
analysis. I doubt that is possible without "static declarative type-
checking."

SPARK Ada is for applications that really *must* be correct or people
could die.

I've always wondered... Are the compilers (or interpreters), which take
these programs to machine code, also formally proven correct? And the OS
in which those programs operate, are they also formally proven correct?
And the hardware, microprocessor, electric supply, etc. are they also
'proven correct'?

With all
due respect, most (not all, but most) Python programmers never get
near such programs
and have no idea about how stringent the requirements are. Nor do most
programmers
in general, for that matter. (It's not an insult)

Aug 31 '07 #30

On Aug 30, 10:20 pm, al...@mac.com (Alex Martelli) wrote:

Russ <uymqlp...@sneakemail.comwrote:

...

programs." Any idea how much Python is used for flight control systems
in commercial
transport aircraft or jet fighters?

Are there differences in reliability requirements between the parts of
such control systems that run on aircraft themselves, and those that run
in airports' control towers?

Yes.

Because Python *IS* used in the latter
case, cfr <http://www.python.org/about/success/frequentis/... if
on-plane control SW requires hard-real-time response,

Yes.

that might be a
more credible reason why Python would be inappropriate (any garbage
collected language is NOT a candidate for hard-real-time SW!) than your
implied aspersions against Python's reliability.

Not really relevant, since there is no (or very little) dynamic memory
allocation.

Python really isn't suitable for in-flight controls for various
reasons, and mission critical concerns is a minor one (systems with
less underlying complexity tend to have fewer failure modes). But
mostly it's raw throughput: Python is just too slow. Flight control
computers have to be powerful enough make a ton of mathematical
calculations in a matter of milliseconds, and under strict weight and
power constraints. The cost of running 100 times slower than optimal
is just too high.

At my current project, we're struggling with throughput even though we
use highly optimized code. Python would be completely out of the
question.

Now, control towers don't have these constraints, and system failure
is not nearly as critical, so Python is a better option there.
Carl Banks

Aug 31 '07 #31

On Aug 30, 9:41 pm, Paul Rubin <http://phr...@NOSPAM.invalidwrote:

Bruno Desthuilliers <bdesth.quelquech...@free.quelquepart.frwrites:
FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained"
why one can not hope to "write reliable programs" without strict
static declarative type-checking.

I don't know about Eiffel but at least an important subset of SPARK
Ada's DBC stuff is done using static analysis tools (not actually
built into the compiler as it happens) to verify statically
(i.e. without actually running the code) that the code fulfills the
DBC conditions. I don't see any way to do that with Python
decorators.

I don't see any way to do that in Python with built-in DBC syntax,
either. :)
Carl Banks

Aug 31 '07 #32

Robert Brown <bb****@speakeasy.netwrites:

In any case, I'm still not sure whether it would be useful to integrate DbC
into Python.

I guess I'm a little confused about what it would mean. Suppose you
want to write a function that looks for a value using binary search
in a sorted list, n = bsearch(a,x). The contract is:

precondition: the input list a is sorted.
postcondition: the output is an integer n, such that if
x is an element of the list, then a[n] == x. If x is not
in the list, then n is -1.

This is a reasonable application of dbc since the precondition and
postcondition are easy to specify and check, but the binary search
algorithm is tricky enough to be susceptible to implementation errors.

The trouble is, the obvious way to write the precondition and
postcondition take linear time, while the binary search should take
log(n) time. In the traditional unit test approach, that's ok, you'd
run the test as part of the build process but not each time the
function is actually called. With something like SPARK/Ada (and maybe
Eiffel), you'd statically validate the conditions. But in Python, the
check occurs at runtime unless you disable it, famously compared to
wearing your parachute on the ground but taking it off once your plane
is in the air.

I guess one difference from unit test philosophy is that at least
sometime, you'd run the entire application with all the dbc checks
enabled, and just live with the slowdown.

Aug 31 '07 #33

Roy Smith

Carl Banks <pa************@gmail.comwrote:

Python really isn't suitable for in-flight controls for various
reasons, and mission critical concerns is a minor one (systems with
less underlying complexity tend to have fewer failure modes). But
mostly it's raw throughput: Python is just too slow. Flight control
computers have to be powerful enough make a ton of mathematical
calculations in a matter of milliseconds, and under strict weight and
power constraints. The cost of running 100 times slower than optimal
is just too high.

I'm not convinced that's true for all avionics uses. Certainly, if you're
doing the fly-by-wire stability control system for a dynamically unstable
airframe, you need a lot of compute power and guaranteed real-time response
(recovery from a VMC rollover is no time for garbage collection). But, not
everything in an airplane is like that.

Take something relatively complicated like a GPS. The basic receiver is
pretty compute intensive, but that's likely to be a dedicated chip. Most
of the functionality in the box, however, requires a lot less horsepower.
You need to handle user input (i.e. keep up a scan on maybe 20 keys), and
update a low-res display (320 x 240 x 8 bit color is typical) with text or
cartoon graphics. There are certain real-time calculations which need to
be done, such as time, distance, and bearing to the next waypoint, but
these are typically updated a few times a second.

Like most things that use Python (or TCL, or Ruby, or ...), I would expect
that most of the low-level stuff would be done in something like C and
Python would be used for the glue code and things where there's no time
pressure.

Aug 31 '07 #34

Russ

I've always wondered... Are the compilers (or interpreters), which take
these programs to machine code, also formally proven correct?

No, they are not formally proven correct (too complicated for that),
but I believe they are certified to a higher level than your "typical"
compiler. I think that Ada compilers used for certain safety-critical
applications must meet higher standards than, say, GNU Ada, for
example.

And the OS

in which those programs operate, are they also formally proven correct?

Same as above, if I am not mistaken.

And the hardware, microprocessor, electric supply, etc. are they also
'proven correct'?

I think the microprocessors used for flight control, for example, are
certified to a higher level than standard microprocessors.

How would you prove a power supply to be "correct"? I'm sure they meet
higher reliability standards too.

Aug 31 '07 #35

On Aug 31, 3:18 am, Russ <uymqlp...@sneakemail.comwrote:

For the record, the guy I
criticized
made ridiculous assertions about DBC.

And that would be me? Oh my! LOL!
This is not nearly as fun as the guy who explained to Steve Holden how
Python works, but still ... ;)

If you are upset about my criticism of one of your colleagues, please
tell him to quite making
outrageous assertions about something he obviously knows little about.

For the record I read the design by contract book by Meyer
years ago (the first edition) and I could not stomach it.
The paper you mentioned is even worse. Programmers asserting
that a given metodology can give 100% reliable software
are incompetents or liars or both. Period.

Of course there are methodologies which are better than
others (for instance automatic tests are better than
manual tests) and one should try various approaches on
the field.

However, IMNSHO, nowadays design by contract has been superseded
by unit tests and it makes little sense to use it. Once
you have automatic tests and once you make liberal use of
assert statements in your code, you should not feel the need
for more than that. You may think differently of course,
but you should know that I am a ferocious opponent of
heavyweight approaches, huge frameworks, and all that.
Most people in the Python community are. This is why I
think dBC will never enter in the core, and it would be
extremely little used even as a third party library
(BTW, it has already happened).

Michele Simionato

Aug 31 '07 #36

Russ

I guess one difference from unit test philosophy is that at least
sometime, you'd run the entire application with all the dbc checks
enabled, and just live with the slowdown.

Yes, that's right. You don't expect to run efficiently with the self-
test checks activated, but you can test your code more conveniently
and comprehensively than unit tests by simply running your program as
usual -- except with the checks activated. If you do that for any
significant period of time, many bugs will find themselves, I'm sure.

Also, to repeat once again, the embedded self-test (DbC) checks can be
used for unit testing too. You simply activate the self-tests when you
do your unit testing, and wait for them to throw exceptions. So it
seems to me that you've killed two birds with one stone.

Aug 31 '07 #37

Russ

Python really isn't suitable for in-flight controls for various
reasons, and mission critical concerns is a minor one (systems with

Do you know anything about the FAA certification process for flight-
critical systems? I am not an expert on it, but I know it is very
expensive. If I am not mistaken, getting such code certified is more
expensive than developing it in the first place. Why would that be so
if, as you claim, "mission critical concerns is a minor one"?

Aug 31 '07 #38

On Fri, 31 Aug 2007 01:15:04 -0400, Roy Smith wrote:

Carl Banks <pa************@gmail.comwrote:
>Python really isn't suitable for in-flight controls for various
reasons, and mission critical concerns is a minor one (systems with
less underlying complexity tend to have fewer failure modes). But
mostly it's raw throughput: Python is just too slow. Flight control
computers have to be powerful enough make a ton of mathematical
calculations in a matter of milliseconds, and under strict weight and
power constraints. The cost of running 100 times slower than optimal
is just too high.

I'm not convinced that's true for all avionics uses.

Of course it's not. I was talking about flight control, not avionics in
general. (Perhaps when single-engine Cessnas go digital we'll even see
flight controllers in Python.)
Carl Banks

Aug 31 '07 #39

On Thu, 30 Aug 2007 22:56:54 -0700, Russ wrote:

>Python really isn't suitable for in-flight controls for various
reasons, and mission critical concerns is a minor one (systems with

Do you know anything about the FAA certification process for flight-
critical systems? I am not an expert on it, but I know it is very
expensive. If I am not mistaken, getting such code certified is more
expensive than developing it in the first place. Why would that be so
if, as you claim, "mission critical concerns is a minor one"?

I made no such claim; you misconstrued what I wrote. I wrote that
mission critical concerns are a minor reason why Python is not used, not
that mission critical concerns were minor.

As a matter of fact, FAA cert is a major pain, and they unit test the
hell out of everything. I'm not aware of any reason why Python couldn't
be certified if it passed the tests, but it likely wouldn't pass as
easily as a compiled language. OTOH, spiffy features like design-by-
contract aren't going to improve your chances of getting FAA cert, either.
Carl Banks

Aug 31 '07 #40

Russ a écrit :

>FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained" why
one can not hope to "write reliable programs" without strict static
declarative type-checking.

And they are probably right.

And they are obviously wrong, by empiric experience.

I don't think you understand what they mean by "reliable
programs."

I think you should stop over-estimating yourself, and start realizing
that there are quite a lot of experimented programmers here.

The important question is this: why do I waste my time with bozos like
you?

The same question is probably crossing the mind of quite a lot of people
here - but the 'bozo' might not be who you think.

Aug 31 '07 #41

On Aug 31, 10:02 am, Russ <uymqlp...@sneakemail.comwrote:

>
Hi Alex. I've always enjoyed your Piggies talks at
Google (although I missed he last one because I was out
of town). I'm disappointed to see that you seem to have
taken personal offense from remarks I made to someone else who
attacked me first.

I am curious. Why do you think I attacked you? The conversion went as
follows:

On Aug 29, 7:21 am, Russ <uymqlp...@sneakemail.comwrote:
>Thanks for that information. That's too bad, because it seems like a
strong positive capability to add to Python. I wonder why the cold
reception. Were there problems with the idea itself or just the
implementation? Or is it just a low priority?

me:
Why do you think that would ad a strong positive capability?
To me at least it seems a big fat lot of over-engineering, not
needed in 99% of programs. In the remaining 1%, it would still not
be needed since Python provides out of the box very powerful
metaprogramming capabilities so that you can implement
yourself the checks you need, if you really need them.

Basically you said "I think DbC is good" and I said "I don't think
so".
I would not call that an attack. If you want to see an attack, wait
for
Alex replying to you observations about the low quality of code at
Google! ;)

Michele Simionato

Aug 31 '07 #42

Michele Simionato <mi***************@gmail.comwrites:

http://archive.eiffel.com/doc/manual...ct/ariane/page...

That paper contains only a good think: a link to the contrarian view
http://home.flash.net/~kennieg/ariane.html#s3.1.5

I like the contrarian article much better than the Eiffel sales pitch.

Aug 31 '07 #43

=?ISO-8859-1?Q?Ricardo_Ar=E1oz?=

Russ wrote:

>I've always wondered... Are the compilers (or interpreters), which take
these programs to machine code, also formally proven correct?

No, they are not formally proven correct (too complicated for that),
but I believe they are certified to a higher level than your "typical"
compiler. I think that Ada compilers used for certain safety-critical
applications must meet higher standards than, say, GNU Ada, for
example.

And the OS
>in which those programs operate, are they also formally proven correct?

Same as above, if I am not mistaken.

>And the hardware, microprocessor, electric supply, etc. are they also
'proven correct'?

I think the microprocessors used for flight control, for example, are
certified to a higher level than standard microprocessors.

How would you prove a power supply to be "correct"? I'm sure they meet
higher reliability standards too.

In that case why don't we just 'certify to a higher level' the programs
and get done with this formal proofs? We should remember that the level
of security of a 'System' is the same as the level of security of it's
weakest component, so either we formally prove all those other very
important components (OS gets MUCH more use than the program (the
program uses it for almost every other action)) or get done with the
whole fuss.

Aug 31 '07 #44