Re: Problems with SPARK 2015 and XMLAda

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

On Fri, 21 Aug 2015 12:43:53 +0200, Stefan.Lucks@uni-weimar.de wrote:

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

Not the callee, only the interface (contract) of.

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

Does not make sense #1 decoupling of callee from callers or that #2 this is
a major design principle?

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

Because with exceptions all this will be implemented by the compiler.

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

That is true, because contracts and proofs, presently, cannot be gradually
refined. And because the contracts of the core Ada are too weak or absent
(as in the case of exceptions). The must be work done to refine
Constraint_Error, Storage_Error, Program_Error contracts.

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

Yes, and this situation must be changed because contracts and proofs are
too valuable to be ignored.

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

SPARK must be an integral part of Ada.

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

But it could have them tomorrow.

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

Really? When reading character by character you must check the code for
each single character. Actually, if honestly implemented, the approach
requires checking after each single language statement for error codes for
memory access violation, stack overflow, integer overflow, floating point
overflow, it is probably an infinite list, which is self-recursive because
check is a statement as well. This is semantically impossible because
checks involve invariants of higher abstractions, e.g. objects, groups of
objects, invariants which can hold in some context and do not hold in
others etc. Error code contradicts to basic principles of software
decomposition.

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