Does Python really follow its philosophy of "Readability counts"?

Paul Rubin http
Tue Jan 20 08:05:57 CET 2009

"Tim Rowe" <digitig at> writes:
> Unless it's changed since I used it, technically, SPADE doesn't allow
> or disallow anything. 

Right, it's an external tool, like pylint; you can still compile code
that SPADE complains about.  Sorry if I wan't more clear.  I just
meant SPADE would flag the code.

> Since the value appears to come from a sensor, the only way one
> could prove that there would be no overflow would be to state it as
> a part of the specification of what is read in. If that
> specification doesn't match the specification of the actual sensor,
> that's nothing to do with the programming language or, for that
> matter, the program itself.  It's a specification mismatch.

Right, that's the point, the assumption about the sensor reading being
in a certain range would have to stated in the specification rather
than implicit in the code; and as such, the problem would more likely
to have been caught at the systems engineering level.

> I was actually at the European Space Agency's Toulouse site the week
> after the Ariane 5 incident. I've been at jollier funerals. I can't
> help thinking that thinking that the team would have benefited from
> reading David Parnas's work on the specification of the A-7E avionics.

Later there was a static analysis of the Ariane code by Cousot et al,
that flagged the error.  I haven't yet looked up the paper to see
exactly what it found.

More information about the Python-list mailing list