Re: Problems with SPARK 2015 and XMLAda

[Stefan.Lucks@uni-weimar.de]

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

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

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

That is Ada. The caller needs to "with" the package where the callee is 
defined, anyway.

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

That := "Since the callee ... to exception.";

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

Wait a minute -- why did you write "re-implement", rather than 
"implement"?

Trying to convert an existing big Ada implementation into SPARK would be a 
very tedious pice of work, regardless of exceptions versus error codes. I 
am inclined to say, this would be futile from the very beginning.

A fresh project, starting from the scratch, would be entirely different.

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

Agreed! If you have a big code base in Ada, translating it into SPARK 
would be the highway to hell, or at least mental insanity.

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

Unfortunately, Ada doesn't have contracted exceptions, today.

> Wrong. I/O states are all known at compile time.

My point was that the overhead for handling error codes is neglible for 
these cases.

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