Re: Problems with SPARK 2015 and XMLAda

["G.B." <bauhaus@futureapps.invalid>]

On 21.08.15 13:56, Dmitry A. Kazakov wrote:
> On Fri, 21 Aug 2015 12:09:43 +0200, G.B. wrote:
>
>> On 21.08.15 11:37, Dmitry A. Kazakov wrote:
>>> Clearly Ada and SPARK must
>>> have had exception contracts which would have statically prevented
>>> unhandled exceptions,
>>
>> Well, it seems a stricture on design to me, if it is to mean:
>> "If implementing my abstraction, though shalt raise but these
>> exceptions: A, B, and C".
>
> The contract can be refined as necessary. E.g. between may and shall raise.
> It is an important thing especially with contracts inherited from
> overridden operations. And there must be transitive contracts, e.g. "*"
> raises this and what "+" does.

O.K.

>> Would He, the designer of exception contracts, by looking into
>> some crystal ball, then write the contract knowing of all
>> possible implementations of the contracted feature in advance?
>
> Certainly so. Because of separation of implementation and interface.

You mean, the designer of contracts with exceptions only needs
to know all possible implementations trivially, correct?
Thus excluding all designs of the feature he might not
have *not* thought of, and need not, due to this formal restriction
banning a choice of exceptions. "You don't need these, my boy!" This has 
consequences.

Like, the consequence
  "You cannot implement the caller and thus you must scrap all your
   design"
does not start from more real
  "You have implemented the caller and thus you cannot scrap all your
   design"

I don't personally need much variability of exceptions, I'd like to
have them in contracts, I use "raises" annotations all the time.
But! Few. Assertion_Error is one.
I also know that exceptions requires adaptable software; I imagine
that programmers will place exception information that is disallowed
by the contract into specially formalized message strings, insofar
as their design requires some handling, but elsewhere.

Or they go "enterprise" and say "An error has occurred".

Uses of contracted exceptions as deplorable as these may outweigh
any advantages.
This is when I'd like exceptions as non-extensible, yet derived
things:

    Drought : exception is new End_Error;

This way, when handling something more specific than End_Error,
"when others =>" could be replaced with a kind of "class-wide"
handler, the class essentially covering related names.

>> Able to decide on which paths of unforeseen computation some
>> implementation might want to give up?
>
> It is not an implementation which does not fulfill the contract, per
> definition of the term "implementation." Sorry about telling basic design
> by contract stuff.

Design by Contract™, which wasn't defined by your or me, has
the "retry" facility as part of the "rescue"(*); both, exceptions as
assertion failures and exceptions as other failures are parts of
the definitions surrounding DbC. But not in the way imagined
here. I'm sure that this imagination of "design by contract" has
somehow definitions of something quite reasonable. It would be
nice, though, if the number of naming conflicts could be small.

It is the possibility of computing possible implementations that
I thought I'd question: designing contracts is a process that
leads to decisions. I am not convinced that shifting responsibility
of handling every non-contracted failure to the implementer
(so as to stay within the allowances of the contract) is going
to be acceptable. Or if so, it will be worked around as outlined
above.

You have reminded us frequently of HALT in connection with
how to predict things in contracts. Do you think that the
*choice* of exceptions is an exception?

__
(*) an older view:
http://se.ethz.ch/~meyer/publications/methodology/exceptions.pdf