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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable 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!weretis.net!feeder4.news.weretis.net!storethat.news.telefonica.de!telefonica.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Fri, 21 Aug 2015 12:43:53 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net> NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: multipart/mixed; BOUNDARY="8323329-1401114337-1440153476=:23776" X-Trace: pinkpiglet.scc.uni-weimar.de 1440154419 24596 141.54.178.228 (21 Aug 2015 10:53:39 GMT) X-Complaints-To: news@pinkpiglet.scc.uni-weimar.de NNTP-Posting-Date: Fri, 21 Aug 2015 10:53:39 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net> User-Agent: Alpine 2.20 (DEB 67 2015-01-07) Content-ID: Xref: news.eternal-september.org comp.lang.ada:27550 Date: 2015-08-21T12:43:53+02:00 List-Id: --8323329-1401114337-1440153476=:23776 Content-Type: text/plain; CHARSET=ISO-8859-15; FORMAT=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE Content-ID: On Fri, 21 Aug 2015, Dmitry A. Kazakov wrote: >> If an exception cannot be handled in the caller's context, the caller >> cannot satisfy its own postconditions. See above! > > Exactly! You cannot implement the caller and thus you must scrap all your > design (decomposition into modules like caller and callee). That is Ada. The caller needs to "with" the package where the callee is=20 defined, anyway. >>> Since the callee shall not know its callers, which is one of the major >>> software design principles, there is no way how return code could be a >>> substitute to exception. >> >> Hu?????? That does not make any sense to me!!! > > (Which "that"?) That :=3D "Since the callee ... to exception."; > Yes, it must re-implement exception propagation throughout all caller, > existing and potential ones. Wait a minute -- why did you write "re-implement", rather than=20 "implement"? Trying to convert an existing big Ada implementation into SPARK would be a= =20 very tedious pice of work, regardless of exceptions versus error codes. I= =20 am inclined to say, this would be futile from the very beginning. A fresh project, starting from the scratch, would be entirely different. > Massive distributed redesign of all client code base. Not a disadvantage, > indeed, it is a catastrophe. Agreed! If you have a big code base in Ada, translating it into SPARK=20 would be the highway to hell, or at least mental insanity. >> One thing that is frightening about exceptions is that by not handling >> locally declared exceptions, some global caller's caller cannot handle >> that specific exception at all -- it can only use *the* *same* catch-all >> >> when others =3D> ...; > > That is true for non-contracted exceptions only. Clearly Ada and SPARK mu= st > have had exception contracts which would have statically prevented > unhandled exceptions, including the "when others =3D>" mess. E.g. Finiali= ze > would have "not raising anything" in the contract, which would force you = to > handle all exceptions. Unfortunately, Ada doesn't have contracted exceptions, today. > Wrong. I/O states are all known at compile time. My point was that the overhead for handling error codes is neglible for=20 these cases. Stefan -------- I love the taste of Cryptanalysis in the morning! -------= - www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-luck= s ----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany-= --- --8323329-1401114337-1440153476=:23776--