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

[Tim Rowe]

2009/1/18 Paul Rubin <"http://phr.cx"@nospam.invalid>:

> I.e. the cast was wrong because of the failure of an unstated
> assumption that a certain sensor reading was in a certain range.
> Spark may still have allowed the cast only if the assumption was
> stated explicitly in the specification.

Unless it's changed since I used it, technically, SPADE doesn't allow
or disallow anything. It produces a predicate (a proof obligation)
that you have to prove is always true (or is it always false? It's
been 18 years since I worked on that stuff, and SPADE and MALPAS
produced their proof obligations with opposite values). So it's still
up to you to show that it won't overflow, it just gives you the
predicate calculus expression that you need to do that.

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.

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.

-- 
Tim Rowe