"Tim Rowe" <digi...@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. -- http://mail.python.org/mailman/listinfo/python-list
