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: border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!rt.uk.eu.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Sun, 14 Jul 2013 12:19:20 +0200 Organization: cbb software GmbH Message-ID: <1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net> References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> <1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net> <1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: xkOZ88C3T5fLavXpgyt3vA.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 X-Original-Bytes: 7187 Xref: number.nntp.dca.giganews.com comp.lang.ada:182512 Date: 2013-07-14T12:19:20+02:00 List-Id: On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net... >> Secondly, it does not work anyway. One famous example was given by >> Forsythe >> in his book on numerical methods. It is solving quadratic equation using >> school formula. In some cases (when roots are close to each other) the >> accuracy catastrophically drops for one root and increases for another. >> You >> *cannot* catch such stuff through tests. Only analysis can, and analysis >> is >> equivalent to proofs. > > If your "cookbook" is full of bad algorithms, then of course you'll get > garbage. And I certainly agree you can't test accuracy. The problem is that > even if you prove that your algorithm is too inaccurate, what can you do? This is a different question. The first one how do I prove things about accuracy. And the answer is that I need bodies to do that and specifying accuracy through contracts would be extremely difficult. Answering the question, if you know that the aircraft will crash, you don't board it. > You don't have any other way to implement it (because you already did the > research to find the best algorithm available -- if you didn't do at least > that, "proof" is the LEAST of your problems). There is practically never the best algorithm. In any case in order to take a decision one needs evidences. The only reliable evidence is a proof. >>>> No, the alternative is to prove that the constraint is not violated. >>> >>> That's completely impractical. >> >> You *always* can do on the client's side: >> >> exception >> when Constraint_Error => >> Put_Line ("Oops!'); >> end; > > That doesn't prove that the constraint is not violated It handles violation, which cannot be prevented otherwise. > You've got to prevent the exceptions at the source, and the main way you do > that for Constraint_Error is to use proper range constraints and null > exclusions on parameters. No. Dynamic constraints cannot prevent anything. They are a part of defining semantics so that violation could be handled elsewhere. Only static constraints can serve prevention. If you let Constraint_Error propagation, you already gave up with static constraints and with provability on the whole class of all instances. You still can have it provable on per instance basis and this is the client's side. > Then your proof is actually possible because we > moved it from inside of the body to the call site. Yes. Bodies are needed. >>>> You can do this only at the client side. Which is why it cannot be >>>> contracted for the callee. When you move from instances to universally >>>> holding contracts you frequently lose provability. >>> >>> ...of things that aren't worth proving in the first place. You get rid of >>> constraint_errors from bodies by writing good preconditions, predicates, >>> constraints, and exclusions in the first place. >> >> Really? You can start writing preconditions for +,-,*,/,** defined in the >> package Standard and continue to user defined types and subtypes. If >> anything is totally impractical then the idea to move Constraint_Error from >> post to pre-condition. It is wrong and will never work for anything beyond >> trivial examples. > > Which is amazing because it works for most examples. (It doesn't work for > overflow of "*" very well, but that's the only real issue.) And in any case, > there is no point in moving it for language-defined operators -- both the > compiler and any provers know exactly what they do. It's only for > user-defined subprograms that you need to do so. How are you going to do that for user-defined subprograms using language-defined operations, which are all user-defined subprograms? >>>>> It's annoying that one can't tell between specification errors that >>>>> should >>>>> be contracted and proved away and those that are truly runtime (that >>>>> is, >>>>> a normal part of the implementation); >>>> >>>> That was ARG's decision for Ada 2012, wasn't it? >>> >>> No, it was an effect of Ada 83, which conflated those uses of exceptions. We >>> had to formalize existing practice (we need the ability to add these >>> specifications to existing code without changing any behavior). It would be >>> better for exceptions that we would want to "prove-away" (like >>> Status_Error >>> and Mode_Error in Text_IO) to be strictly separated from those that are >>> purely runtime behavior (like End_Error and Device_Error). >> >> This has nothing with that. >> >> Status_Error and Mode_Error are there because file type as designed does >> not reflect its mode: >> >> type Read_File_Type is ... >> type Write_File_Type is ... >> type Readwrite_File_Type is Read_File_Type and Write_File_Type is ... >> >> Done. > > Huh? This makes no sense for this problem. You can't do that in any version > of Ada (or any other sensible language), Of course I can. It is MI. Even in Ada it is partially possible with interfaces, just a bit more clumsy than it should be. It is trivial to statically ensure that Write will never be called on Read_File_Type. It has no such operation. > because it would require that the > type of a file object could change in response to operations. Never. >>> One thing we had to do is to make these things work is to allow existing >>> compilers to use runtime checks, with the hope that more will become >>> proved over time. Compiler technology isn't quite ready for mandatory proof >>> requirements (maybe next time). >> >> This is a conflation of its worst. > > Carried over from Ada 83. Ada will never be a language that requires much in > the way of proof, it would be way too disruptive to existing > implementations. I don't see how adding optional exception contracts should disrupt anything. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de