From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Fri, 21 Aug 2015 09:30:46 +0200 Organization: cbb software GmbH Message-ID: References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:27542 Date: 2015-08-21T09:30:46+02:00 List-Id: On Fri, 21 Aug 2015 08:26:53 +0200, Stefan.Lucks@uni-weimar.de wrote: > On Thu, 20 Aug 2015, Randy Brukardt wrote: > >> SPARK forces such errors to be reported as error codes, and that's pure >> evil. > > There are two cases against error codes, a strong one and a weak one. > > The strong case that programmers just tend to forget handling them, or > even intentionally ignore them. This is why error codes are evil. > > But this is a non-issue for SPARK: If the postconditions of a subprogramm > allow error codes, the caller cannot ignore the error and still prove its > own postconditions (at least for any sort of useful postconditions). > > The weak case is about readability. It is a reason why error codes are > bad, but not quite evil. And it actually is an issue for SPARK: > > Source code with well-used exception handlers at the bottom of a block are > often better readable than programs where the error-handlers are > distributed across the source code, with an error handler after every > program call returning an error code. No, it is not about readability or dangers of not testing the return code. The main reason is that exceptions indicate states which usually cannot be handled on the caller's context. (All other applications, e.g. to indicate bugs are illegitimate) Whatever the code is, unless indicating "success", some callers cannot do anything with that and should pass it to their callers and maybe to the caller's caller and so on. The idea of exception is that the caller *cannot continue* when the callee detected an exceptional state. Since the callee shall not know its callers, which is one of the major software design principles, there is no way how return code could be a substitute to exception. You must rework the design and contaminate the code of all callers up the calling chain until continuation were logically possible. Another reason is distributed overhead of testing return codes. Modern compilers and processors have zero exception overhead when no exception raised. Exceptions, when used properly, are rare, thus programs using exceptions could be far more efficient. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de