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.241.162 with SMTP id wj2mr4929695pbc.2.1340632480512; Mon, 25 Jun 2012 06:54:40 -0700 (PDT) Path: l9ni18368pbj.0!nntp.google.com!news1.google.com!goblin3!goblin1!goblin.stu.neva.ru!newsfeed.straub-nv.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Mon, 25 Jun 2012 16:08:01 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: 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: stefan-lucks@see-the.signature NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 X-Trace: tigger.scc.uni-weimar.de 1340632479 5919 141.54.178.228 (25 Jun 2012 13:54:39 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Mon, 25 Jun 2012 13:54:39 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> Content-Type: TEXT/PLAIN; charset=US-ASCII Date: 2012-06-25T16:08:01+02:00 List-Id: 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. ;-) 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. But back to the real topic. > 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. But actually, by choosing that axiom as your logical starting point, you have made several logical errors by yourself. *Firstly*, you don't seem to separate between syntax and semantic. Ada 2012 provides pre- and postconditions (and also invariants) allow to *specify* contracts. That is a great advantage over writing more or less informal contracts -- and even to SPARK's annotations inside Ada comments. This is a syntax for specifications, no more, no less! What is wrong with that syntax? If you like SPARK, you should welcome it! So much about syntax, now comes the semantic. *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 The language requires the compiler to support the first two, but the language allows the third one just as well. I anticipate that we will soon see tools to support proving Ada 2012 annotations statically. Even SPARK may soon support the Ada 2012 syntax for its annotations. *Thirdly*, you seem to assume that a tool that can be used in a destructive way cannot also be used properly. 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. Which is what you try do do without dynamic checks, or by writing your pragma Assert(...) in current Ada, just as well! Used that way, dynamic checks in Ada 2012 will ease testing and debugging. Which is good! -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- ------ I love the taste of Cryptanalysis in the morning! ------