"Russ P." <russ.paie...@gmail.com> writes: > I don't know which variant of Ada was used here, but something called > the "Ravenscar Profile" is a reduced subset of Ada that might have > prevented this error (though I haven't verified this). Then there is > Spark Ada, which supposed to be much safer than even Ada.
I'm not sure, but I think Ravenscar and Spark would both have permitted the cast. However, Spark is intended to be used with an external tool called Spade (sort of a Pylint on steroids) that would not have allowed the cast unless it was provable (starting from the specification) that the number was in range before the cast. 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. Requiring the assumption to be stated may have made the error more likely to be spotted as part of the surrounding systems engineering. Of course, the specification can still be wrong, but that's hardly a problem with Ada or even with the software. It's not too much different than if the specification says the rocket is 10 feet wide and they build the launch pad for that size, but then the rocket turns out to actually be 12 feet wide. I have Barnes's book about Spark at the office and will try to check next week what it says about these casts. -- http://mail.python.org/mailman/listinfo/python-list
