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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Fri, 21 Aug 2015 13:56:28 +0200 Organization: cbb software GmbH Message-ID: <1j3alqfkzrx0r$.1gv7vbgpembl4$.dlg@40tude.net> References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:27551 Date: 2015-08-21T13:56:28+02:00 List-Id: 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