From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Problems with SPARK 2015 and XMLAda
Date: Fri, 21 Aug 2015 12:09:43 +0200
Organization: A noiseless patient Spider
Message-ID: <mr6ta0$aq3$1@dont-email.me>
References: <e3de50ce-e994-4038-8160-13266aeb207e@googlegroups.com>
 <lymvxn112j.fsf@pushface.org>
 <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com>
 <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com>
 <mr5dnn$ce9$1@loke.gir.dk> <alpine.DEB.2.20.1508210804480.22981@debian>
 <puak04qc3k8o$.1epetyorakzeg$.dlg@40tude.net>
 <alpine.DEB.2.20.1508210948320.23241@debian>
 <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 21 Aug 2015 10:08:00 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="11075"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX184gLv+8M4Urck8PyrRjg++tJWSmxEGQI8="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0)
 Gecko/20100101 Thunderbird/38.2.0
In-Reply-To: <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net>
Cancel-Lock: sha1:KpqJ/cfFcOBub72koXRt/1Id8Lo=
Xref: news.eternal-september.org comp.lang.ada:27548
Date: 2015-08-21T12:09:43+02:00
List-Id: <comp.lang.ada>

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