Re: Problems with SPARK 2015 and XMLAda

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

On Fri, 21 Aug 2015 15:46:58 +0200, G.B. wrote:

> On 21.08.15 13:56, Dmitry A. Kazakov wrote:
>> On Fri, 21 Aug 2015 12:09:43 +0200, G.B. wrote:
>>
>>> 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?

The designer of the exceptions contract needs to know what he wants to
impose on the implementations to make client design robust.

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

He must, because the clients will rely on the contract. He would avoid too
rigid contracts, sure.

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

That is not such a big problem as it appears. The designer of the contract
can include may raise Constraint_Error or Data_Error. This would not weaken
the design of the implementation, which, still, can strengthen the
post-condition to "I don't raise Constraint_Error." The prover will use the
*concrete* client contract of the implementation, to see that the client
does not need to handle Constraint_Error when it does not pass it further.

The important thing is that the prover deals with actual contracts, unless
it is generic programming (sets of implementations).

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

Programmers misuse language features. A good language design is to prevent
them doing this.

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

This is another discussion: whether exception is a value of an indefinite
type (Ada) or of a type hierarchy (C++). Both have advantages and
disadvantages. Contracted exceptions would gravitate to the former.

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

I don't care about trade marks. I do about the meanings.

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

A contract that is not fulfilled is not a contract. Of course you can
redesign any contract during the software developing cycle, that is no
problem, except for the costs. But no implementation exists prior the
contract and no code is an implementation if it breaches the contract.
Simple, isn't?

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

No.

Contract is not an implementation. A contract is a constraint put on the
set of possible implementations. Halting problem equivalence is a handy
tool to illustrate that the set of implementations cannot be reduced to a
singleton instance. Which is why contract /= implementation.

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