On Tue, 2005-02-08 at 18:42 +0100, Lorens Kockum wrote: > > For high-assurance code, exceptions must surely be dealt with, and it is > > appropriate to state a theorem that the application doesn't throw any. > > It *may* be appropriate to state theorems that a given procedure f() > > only throws certain exceptions (which is a good bit stronger than just > > declaring them). > > Sorry, but I don't see the practical difference.
There is no difference in high assurance code. The difference lies in low-assurance code, where it is perfectly okay that an exception should go uncaught and let the application fail in rare circumstances, but not at all acceptable for the application to utterly fail to run due to what was, in effect, an incompatible upgrade that was incompatible because of a language restriction. > You're saying that listing all exceptions thrown by a function > should be a theorem or part of a theorem relative to the > function. I agree with that. The difference is that as I > understand it, a function does not have to have a theorem > assigned to it, but in java the list of exceptions must be > declared. If the list of exceptions is a theorem, then all > functions must have a theorem; that is definitively pulling > developers into the theorem definition world. Yes. Given which I would prefer to do this with a theorem than with an exception declaration. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
