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: border1.nntp.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!feeder02.blueworldhosting.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!newsfeed.fsmpi.rwth-aachen.de!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Tue, 16 Jul 2013 17:13:43 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> <1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net> <1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net> <1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net> <1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1374012824 27612 69.95.181.76 (16 Jul 2013 22:13:44 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 16 Jul 2013 22:13:44 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-Original-Bytes: 11098 Xref: number.nntp.dca.giganews.com comp.lang.ada:182535 Date: 2013-07-16T17:13:43-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net... > On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" wrote in message >> news:1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net... >>> On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote: >> ... >>>> 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. >> >> Sorry, you definitely can prove that dynamic constraints can't be >> violated. > > Only in some cases. For proofs it must be all or nothing. > >> Ada compilers do it all the time. The issue is letting the programmer >> have >> access to that information. > > This is upside down. The programmer should manifest his intention for a > constraint to hold and the compiler should verify that. The manifest must > be syntactically visible. Conflation such declaration with dynamic > constraints is a bad idea. Yes, that's precisely what I'm talking about - some sort of exception contract. But those don't depend on the kind of constraint. >>> 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. >> >> If you don't want Constraint_Error to propagate (and generally one does >> not), then you don't put that into the exception contract for the >> routine. > > This would make the routine non-implementable, because, again, you cannot > do that on the callee side. It is a halting problem. As you showed a couple of days ago, it's trivial on the callee side (just stick in a handler). The hope is to use proof techniques to reduce the cases where that's required, but I see no important reason to worry about eliminating that. >>> You still can have it provable on per instance basis and this is the >>> client's side. >> >> No, that's making a lot more complicated that it needs to be, and I don't >> think it's possible in any useful generality. > > SPARK does this already. Exactly my point! :-) > Moreover historically the concept of correctness > proofs was explicitly about instances. Only later, with the dawn of > generic > programming, it was expanded onto contracts and behavior in general (e.g. > LSP). The latter is much more difficult and frequently impossible in hard > mathematical sense (undecidable). Certainly, there is lots of stuff that's not worth proving that's not provable. So what? We've lived for decades without general proof and there is absolutely no evidence that general proof would do anything to improve the quality and timelyness of software. (Software that takes longer to develop isn't viable no matter how much better quality it actualy is.) >> In any case, going that route completely takes the compiler out of the >> equation. Once you do that, only an extremely limited number of users >> would >> care, and there will be no effect on normal programs. > > I disagree. I trust that most Ada programmers will enjoy trying it in > their > program and gradually relaxing requirements on the proofs as they see what > can and what cannot be proved. No one is going to run extra tools beyond compilation; they simply don't have the time. The "win" with Ada is that the extra correctness brought by the language comes for "free", it's an integrated part of the development process. (Your program cannot be run if it doesn't compile.) Extra tools never will have that level force behind them, and people like me would never run them. ... >> Why is there a problem? Every Ada compiler (and pretty much every other >> compiler as well) does it already. > > How do you prove that this does not raise Constraint_Error > > function Geometric_Mean (A, B : Float) return Float is > begin > return sqrt (A * B); > end Geometric_Mean; You can't, because it does. :-) Your contract is not strong enough, which is not surprising: you have unbounded types here -- you can prove nothing about such types. But that's OK, there is no point in proving everything about everything. Moreover, if you made this an expression function (meaning that you are merely giving a name to "sqrt (A*B)", you could plug it in without any effect on your proof. Enjoy. >> The only issue is that programmers can't >> harness it for their own purposes. I would hope that exception contracts >> would be defined in order to do that. > > Yes. But they will only help if used on the client side and when bodies > are > looked into. You might be right, but in that case we're wasting our time even thinking about proof, because any technology that requires programmer-visble access to bodies is evil. ("Evil" here being a shorthand for "has a bunch of bad properties", which I've previously outlined.) And you may say that many Ada compilers have such features, and I repeat that pragma Inline and macro-expanded generics are evil, if they have any programmer-visible effect. Those sorts of things are only acceptable if they are completely semantically invisible, and that is rarely true. > 1. You will not prove that sqrt never raises Constraint_Error. You will do > that in *your* calls to sqrt it never does. You don't have to. A properly written Sqrt has a precondition, and that precondition raises Constraint_Error when it fails. Sqrt itself never raises any exception. You then prove at the call site that the precondition is met. > 2. In a great number of cases you won't be able to contract *when* > Constraint_Error is to be raised. Consider this: > > function Sum (A : Float_Array) return Float; > > You cannot spell the contract when Sum must raise Constraint_Error and > when > not. Such a contract would much more complex (=> error prone) than the > implementation itself. This is why when the caller of Sum contracts itself > not to raise Constraint_Error, you will have to look into the body of Sum > in order to prove that. Otherwise, you will end up with Java's exception > contracts mess and brainless catch-all handlers. Yup, if you think that *everything* can be contracted and should be contracted, the only possible result is Java's mess. That's perfectly clear, because I certainly agree with you that you can't explain why exceptions are raised formally in many cases. And that's actually OK, because the point is to get rid of the exceptions (with smart use of constraints, predicates, and preconditions). If you can't do that, there's really nothing to prove and nothing to be gained from the contracts. ... >> You've never explained how you supposely static approach would work in >> the >> face of failing Opens, among other things. > > It is supposed to work with Read and Write. > > Maybe I didn't understand your point. I didn't say that Open should not > raise Status_Error. I did that Read should not. I agree with that, that's the precondition's job. > Opening readonly file for writing is not a bug it is an error, a legitime > state of the program which must be handled. Writing a file opened as > readonly is a bug. Bug /= error. Errors are handled, bugs are fixed. You claim that you can use the file type to eliminate Status_Error and Mode_Error. But that's impossible, because an Open that fails leaves the file unopened; and you have to be able to fall back and open a different file (or create one instead) on such a condition. It's not practical to have a single Open operation as an initializer -- so your scheme means that the file type has to change dynamically during it's lifetime. That's the purpose of a subtype, not of a type (in Ada terms, at least). >> But you are insisting on more than that, and I think that's actively >> harmful >> to programming in general. You seem to insist on access to bodies even >> with >> such contracts, but that would prevent all compile-time checking -- the >> only >> kind that would benefit most programmers. > > I don't see how allowing correctness checks involving the bodies should > prevent correctness checks involving the specifications. Because you can't have "correctness checks" involving bodies that don't exist. And having them depend on bodies is "evil", because it means that a change to a body can make a call in someone else's code fail. That's completely unacceptable - it would be impossible to write any reusable code in such an environment. >> I want each subprogram to be >> checked in isolation (subject its contracts), because in that case there >> is >> no coupling between calls and bodies. > > This will be too weak to be useful. It was attempted long ago by LSP. LSP is a dynamic thingy, completely uncheckable at compile-time. And you may be right, in which case any sort of proof is worthless, because violating encapsulation instantly causes all of the bad effects that Ada have been designed to avoid -- changing an unrelated thing (and every body is unrelated in Ada terms) never makes someone else's code illegal. Randy.