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." Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Fri, 21 Aug 2015 15:46:58 +0200 Organization: A noiseless patient Spider Message-ID: References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net> <1j3alqfkzrx0r$.1gv7vbgpembl4$.dlg@40tude.net> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 21 Aug 2015 13:45:15 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="b96887e80893c84a90c3007226ca0d1c"; logging-data="26527"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18hpn0eumZgBpH5O2SUz5a6w4w0LYirCoI=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.2.0 In-Reply-To: <1j3alqfkzrx0r$.1gv7vbgpembl4$.dlg@40tude.net> Cancel-Lock: sha1:PbIm0FtRgrmYTEgJjG42ULsD9L8= Xref: news.eternal-september.org comp.lang.ada:27554 Date: 2015-08-21T15:46:58+02:00 List-Id: On 21.08.15 13:56, Dmitry A. Kazakov wrote: > 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. O.K. >> 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. You mean, the designer of contracts with exceptions only needs to know all possible implementations trivially, correct? Thus excluding all designs of the feature he might not have *not* thought of, and need not, due to this formal restriction banning a choice of exceptions. "You don't need these, my boy!" This has consequences. Like, the consequence "You cannot implement the caller and thus you must scrap all your design" does not start from more real "You have implemented the caller and thus you cannot scrap all your design" I don't personally need much variability of exceptions, I'd like to have them in contracts, I use "raises" annotations all the time. But! Few. Assertion_Error is one. I also know that exceptions requires adaptable software; I imagine that programmers will place exception information that is disallowed by the contract into specially formalized message strings, insofar as their design requires some handling, but elsewhere. Or they go "enterprise" and say "An error has occurred". Uses of contracted exceptions as deplorable as these may outweigh any advantages. This is when I'd like exceptions as non-extensible, yet derived things: Drought : exception is new End_Error; This way, when handling something more specific than End_Error, "when others =>" could be replaced with a kind of "class-wide" handler, the class essentially covering related names. >> 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. Design by Contract™, which wasn't defined by your or me, has the "retry" facility as part of the "rescue"(*); both, exceptions as assertion failures and exceptions as other failures are parts of the definitions surrounding DbC. But not in the way imagined here. I'm sure that this imagination of "design by contract" has somehow definitions of something quite reasonable. It would be nice, though, if the number of naming conflicts could be small. It is the possibility of computing possible implementations that I thought I'd question: designing contracts is a process that leads to decisions. I am not convinced that shifting responsibility of handling every non-contracted failure to the implementer (so as to stay within the allowances of the contract) is going to be acceptable. Or if so, it will be worked around as outlined above. You have reminded us frequently of HALT in connection with how to predict things in contracts. Do you think that the *choice* of exceptions is an exception? __ (*) an older view: http://se.ethz.ch/~meyer/publications/methodology/exceptions.pdf