Re: Problems with SPARK 2015 and XMLAda

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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