status of Programming by Contract (PEP 316)?

[Chris Mellon]

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.

 

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

 

[Russ]

Russ a écrit :
(snip)


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.

 

[Chris Mellon]

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

 

[Russ]

Russ a écrit :

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.

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.

 

[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/
@returns(list)
def makelist(a, b, c):
return [a, b, c]

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

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

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

 

[Russ]

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.

 

[Russ]

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.

 

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

 

[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?

 

[Paul Rubin]

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.

 

[Russ]

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)

 

[Alex Martelli]

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

According to
<http://uptime.pingdom.com/site/month_summary/site_name/www.google.com>,
Google's current uptime is around 99.99%, with many months at 100% and a
few at 99.98% -- and that's on *cheap*, not-that-reliable commodity HW,
and in real-world conditions where power can go away, network cables can
accidentally get cut, etc. I'm Uber Tech Lead for Production Systems at
Google -- i.e., the groups I uber-lead are responsible for some software
which (partly by automating things as much as possible) empowers our
wondrous Site Reliability Engineers and network specialists to achieve
that uptime in face of all the Bad Stuff the world can and does throw at
us. Guess what programming language I'm a well-known expert of...?

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

Yeah, good question indeed, and I'm asking myself that -- somebody who
posts to this group in order to attack the reliability of the language
the group is about (and appears to be supremely ignorant about its use
in air-traffic control and for high-reliability mission-critical
applications such as Google's "Production Systems" software) might well
be considered not worth responding to. OTOH, you _did_ irritate me
enough that I feel happier for venting in response;-)

Oh, FYI -- among the many tasks I undertook in my quarter-century long
career was leading and coordinating pilot projects in Eiffel for one
employer, many years ago. The result of the pilot was that Eiffel and
its DbC features didn't really let us save any of the extensive testing
we performed for C++-coded components, and the overall reliability of
such extensively tested components was not different in a statistically
significant way whether they were coded in C++ or Eiffel; Eiffel did let
us catch a few bugs marginally earlier (but then, I'm now convinced
that, at that distant time, we used by far too few unit-tests for early
bug catching and relied too much on regression and acceptance tests),
but that definitely was _not_ enough to pay for itself. DbC and
allegedly rigorous compile-time typechecking (regularly too weak due to
Eiffel's covariant vs countervariant approach, btw...), based on those
empirical results, appear to be way overhyped.

A small decorator library supporting DbC would probably be a nice
addition to Python, but it should first prove itself in the field by
being released and supported as an add-on and gaining wide acceptance:
"arguments" such as yours are definitely NOT going to change that.


Alex

 

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

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'?

 

[Carl Banks]

...


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

 

[Carl Banks]

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

 

[Robert Brown]

DbC and allegedly rigorous compile-time typechecking (regularly too weak
due to Eiffel's covariant vs countervariant approach, btw...), based on
those empirical results, appear to be way overhyped.

My experience with writing Eiffel code was a bit different. Integrating
code from multiple sources happened much faster than I expected, and the
code ran reliably. There were a couple of instances where previously
uncombined code was linked together and worked on the first run.

Perhaps more important, however, is that method contracts provide important
documentation about how each method is supposed to work -- what it assumes
and what must be true when it returns. Using Eiffel changed my coding
process. Often I'd write the pre- and postconditions first, then write the
method body, just as programmers today often write unit tests first.
Thinking carefully about the contracts and writing them down, so they could
be verified, makes the code more reliable and maintainable. The contracts
are part of the source code, not a fuzzy concept in each programmer's head.

The contracts are also useful when discussing the code with domain experts
who are not programmers. They can read and understand the "flat short" view
of a class, which includes all the method names, method comments, and
contracts, but leaves out the method implementations. Here's an example,
Eiffel's String class: http://www.nenie.org/eiffel/flatshort/string.html

In any case, I'm still not sure whether it would be useful to integrate DbC
into Python. A library that implements DbC for Common Lisp has not gotten
much traction in that community, which has a similar style of software
development. Perhaps it's just too much to ask that programmers write both
unit tests and method contracts.

bob

 

[Paul Rubin]

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.

 

[Roy Smith]

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.

 

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