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 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.227.67 with SMTP id ry3mr9621152pbc.8.1340634967554; Mon, 25 Jun 2012 07:36:07 -0700 (PDT) Path: l9ni18488pbj.0!nntp.google.com!news1.google.com!news4.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!194.109.133.85.MISMATCH!newsfeed.xs4all.nl!newsfeed6.news.xs4all.nl!xs4all!newsgate.cistron.nl!newsgate.news.xs4all.nl!news2.euro.net!news.mixmin.net!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Mon, 25 Jun 2012 16:36:09 +0200 Organization: cbb software GmbH Message-ID: <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net> References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <4fe59ea0$0$9502$9b4e6d93@newsspool1.arcor-online.net> <1mkp7fzlk1b0y.1ueinfjn48fcy$.dlg@40tude.net> <4fe72b6b$0$9504$9b4e6d93@newsspool1.arcor-online.net> <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net> <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net> <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-06-25T16:36:09+02:00 List-Id: On Mon, 25 Jun 2012 16:08:01 +0200, stefan-lucks@see-the.signature wrote: > I am not sure if I can cool down this heated discussion, but I'll give it > a try. > > On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > >> On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote: >> >>> Indeed, it helps to remember that logicians and mathematicians >>> have learned that logic and mathematics cannot justify themselves. >> >> No, they never ever did that. From very beginning mathematicians used >> axiomatic approach instead. What they did, was constructing frameworks >> within which one could not deduce both A and not A. > > A bit off topic -- but this is not quite true. > > Firstly, the axiomatic approach has become mathematical mainstream only > since about the times of David Hilbert. The "very beginning" of > Mathematics and Logic are quite a bit earlier. ;-) Euclid > Secondly, Hilbert's program was to construct frameworks being both > complete (all correct conclusions should be deducible) and one should not > be able to deduce both A and not A. Kurt Goedel eventually showed that > this is *logically* impossible. Hilbert's program by no means was intended to justify logic or mathematics themselves. This is outright wrong. >> Is SPARK nothing? Is strong typing nothing? >> >> But you seemingly did not read what I wrote earlier. There is either #1 or >> #2. > > This the axiom that *you* choose to start with. Starting from there, your > reasoning may be logically correct. If Ada precondition is neither implementation (#1) nor specification/contract (#2) then what is it? Since nobody ever came with #3, I considered only #1 and #2. > *Firstly*, you don't seem to separate between syntax and semantic. I said nothing about the syntax. It could be better, but syntax is always the most difficult part. > *Secondly*, you seem to overlook that there are three semantical options, > rather than the two you mention: > > 1 ignore the conditions > > 2 check them dynamically at run time > > 3 prove them statically at compile time I didn't: Assuming #1, only no.2 is possible. #1 <=> no.2 Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or no.2. One *cannot* mix no.1/3 with no.2, that is what upsets me. > Even SPARK may soon support the Ada 2012 syntax for its annotations. That is OK to me, however, considering syntax I wished a clearer separation of pre-/post-conditions from other declarations. But since GPS rules, I suppose it would not be much difficult to have a view cutting pre-/post-conditions off and displaying them in a side-by-side window scrolled upon mouse hovering etc. > *Thirdly*, you seem to assume that a tool that can be used in a > destructive way cannot also be used properly. In this particular case (#2 + no.3) we wave a very strong evidence: accessibility checks. It was a disaster. > The support for the second option is such a tool. I agree with you, any > program that claims some preconditions, postconditions and invariants > should stop and must be fixed when any such check fails. Silently handling > the exception and then continuing is > > - a logical contradiction in itself, and also > > - the result from some lousy programming practice. > > There is no justification for handling the exception instead of fixing the > flaw! > > But the same tool can properly be used for debugging and testing -- if any > assertion fails, and you detect this at run time, write all relevant > details into a log file, stop the program, and fix the bug. No objection whatsoever. I covered this case earlier. It is OK to check dynamically under the condition that the checker is an *independent* program. A debugger, checker, reasonably protected Ada run-time verifying preconditions and *handling* failed checks is perfectly consistent and advisable. That clearly precludes no.2: handling is within the checker, checker is outside the testee. And, very importantly, we want to contract exceptions some day, don't we? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de