Re: Problems with SPARK 2015 and XMLAda

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

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.

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

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

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