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 14:35:50 +0200 Organization: cbb software GmbH Message-ID: 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:27552 Date: 2015-08-21T14:35:50+02:00 List-Id: On Fri, 21 Aug 2015 12:43:53 +0200, Stefan.Lucks@uni-weimar.de wrote: > 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 > defined, anyway. Not the callee, only the interface (contract) of. >>>> 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 := "Since the callee ... to exception."; Does not make sense #1 decoupling of callee from callers or that #2 this is a major design principle? >> 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 > "implement"? Because with exceptions all this will be implemented by the compiler. > Trying to convert an existing big Ada implementation into SPARK would be a > very tedious pice of work, regardless of exceptions versus error codes. I > am inclined to say, this would be futile from the very beginning. That is true, because contracts and proofs, presently, cannot be gradually refined. And because the contracts of the core Ada are too weak or absent (as in the case of exceptions). The must be work done to refine Constraint_Error, Storage_Error, Program_Error contracts. > A fresh project, starting from the scratch, would be entirely different. Yes, and this situation must be changed because contracts and proofs are too valuable to be ignored. >> 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 > would be the highway to hell, or at least mental insanity. SPARK must be an integral part of Ada. >>> 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 => ...; >> >> That is true for non-contracted exceptions only. Clearly Ada and SPARK must >> have had exception contracts which would have statically prevented >> unhandled exceptions, including the "when others =>" mess. E.g. Finialize >> would have "not raising anything" in the contract, which would force you to >> handle all exceptions. > > Unfortunately, Ada doesn't have contracted exceptions, today. But it could have them tomorrow. >> Wrong. I/O states are all known at compile time. > > My point was that the overhead for handling error codes is neglible for > these cases. Really? When reading character by character you must check the code for each single character. Actually, if honestly implemented, the approach requires checking after each single language statement for error codes for memory access violation, stack overflow, integer overflow, floating point overflow, it is probably an infinite list, which is self-recursive because check is a statement as well. This is semantically impossible because checks involve invariants of higher abstractions, e.g. objects, groups of objects, invariants which can hold in some context and do not hold in others etc. Error code contradicts to basic principles of software decomposition. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de