On Sun, 2005-02-06 at 00:59 -0500, Swaroop Sridhar wrote: > But, getting a run-time exception is a little too late. > The product was shipped, and the software (aircraft > controller?) crashed.
Guys, let's stop mixing our examples up. The flight control system is a critical system that should never go into the air unless the runtime exception can be shown not to be thrown. The only class of programs for which the question of default binding for +/- matters is the class where the programmer isn't likely to bother with this theorem. In this case, the programmer has declared (by omission) that they don't care whether the program is right or not. In light of which, our obligation is merely to choose a reasonable balance between efficiency and approximate correctness. > And, if there is a proof obligation > to show that the exception will never occur, we are back > to the same halting problem. I'm sorry, but this just isn't the halting problem. There is ample evidence from Spark/ADA that checking the absence of arithmetic exceptions is feasible in very large programs. They have examples of success on real ADA programs exceeding 1,000,000 lines. > Probably, the best solution in the case of non_mod_+ > and non_mod_- is that if the compiler (to be understood as > compiler-prover combination) is unable to trivially (for > large values of trivially, which is decidable) show that > the expression is guaranteed not to overflow... It would be a very great mistake to place a burden of theorem proving on the compiler. It's perfectly fine to build in to the compiler transforms that have been separately checked by the prover. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
