Re: Problems with SPARK 2015 and XMLAda

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

On Fri, 21 Aug 2015 10:19:50 +0200, Stefan.Lucks@uni-weimar.de wrote:

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

Exactly! You cannot implement the caller and thus you must scrap all your
design (decomposition into modules like caller and callee).

Exceptions are here to make reasonable decomposition possible.

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

Which is impossible to do, as we saw above.

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

(Which "that"?)

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

Yes. The difference is in the callers.

> It must check the error codes of its callees and, in the 
> exceptional case, return its own error code.

Yes, it must re-implement exception propagation throughout all caller,
existing and potential ones.

> This is not necessarily a disadvantage for error codes!

Massive distributed redesign of all client code base. Not a disadvantage,
indeed, it is a catastrophe.

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

That is true for non-contracted exceptions only. Clearly Ada and SPARK must
have had exception contracts which would have statically prevented
unhandled exceptions, including the "when others =>" mess. E.g. Finialize
would have "not raising anything" in the contract, which would force you to
handle all exceptions.

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

These are misuse of exceptions. States not known at compile time (design
time) are bugs. You cannot do anything with bugs in a running program. The
bug handler is you. Bug fixing is accomplished by typing some text in the
IDE, recompiling and deploying the program.

> (as Randy wrote) are usually related to input-output operations.

Wrong. I/O states are all known at compile time. You do know that you might
get a read error. Indeterminism of program's inputs has nothing to do with
compiler-time constants (or indeterminism of the program itself).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de