Does Python really follow its philosophy of "Readability counts"?
Tue Jan 20 08:05:57 CET 2009
"Tim Rowe" <digitig at gmail.com> 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