Re: Problems with SPARK 2015 and XMLAda

[Stefan.Lucks@uni-weimar.de]

[-- Attachment #1: Type: text/plain, Size: 3907 bytes --]

On Fri, 21 Aug 2015, Dmitry A. Kazakov wrote:

I wrote:

>> 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).

Don't forget the two paragraphs above!

>> 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.

If an exception cannot be handled in the caller's context, the caller 
cannot satisfy its own postconditions. See above!

> The idea of exception is that the caller *cannot continue* when the callee
> detected an exceptional state.

The idea of statically proven postconditions with error codes is to force 
the caller to return its own exception code.

> 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.

Hu?????? That does not make any sense to me!!!

Here is some code with exceptions:

   End_Error, Data_Error, Mode_Error, Layout_Error: exception;

   procedure Do_Something(Filename: String);
     -- may raise any of the above exceptions

Here is the same code with error codes substituting the exceptions:

   type Errors is (None, End_Error, Data_Error, Mode_Error, Layout_Error);

   procedure Do_Something(Filename: String; Error: out Errors);

The only thing that is not possible is for a caller to ignore or re-raise 
an exception. It must check the error codes of its callees and, in the 
exceptional case, return its own error code.

This is not necessarily a disadvantage for error codes!

One thing that is frightening about exceptions is that by not handling 
locally declared exceptions, some global caller's caller cannot handle 
that specific exception at all -- it can only use *the* *same* catch-all

   when others => ...;

exception handler for all such exceptions. For error codes, on the other 
hand, the Ada type system ensures that the caller will always know the 
callee's exception codes.

> 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.

I doubt this makes any observable difference. The legitimate examples for 
exceptions that "signal things that cannot be known at compile time" (as 
Randy wrote) are usually related to input-output operations. Your machine 
is so much faster than such external devices that the overhead for a 
comparison like "if Error_Code /= None" would be negligible.

Stefan


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----