Re: Problems with SPARK 2015 and XMLAda

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

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

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?
Able to decide on which paths of unforeseen computation some
implementation might want to give up? Disallowing any other exception
known to both the implementer of the feature and the implementer
of the caller?

Or is it about exceptions written into the contract after knowing
all possible callers, and being able to adjust all source code
as necessary? (I.e., dismissing immutable software components?)