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,ea5071f634c2ea8b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.39.100 with SMTP id o4mr7238759pbk.0.1322121016480; Wed, 23 Nov 2011 23:50:16 -0800 (PST) Path: lh20ni11971pbb.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!news.internetdienste.de!news.tu-darmstadt.de!news.belwue.de!news.uni-stuttgart.de!news-2.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. Date: Thu, 24 Nov 2011 08:46:33 +0100 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net> <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net> <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net> <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net> <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net> <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> <4ecc35b8$0$7628$9b4e6d93@newsspool1.arcor-online.net> <4eccd5d2$0$6637$9b4e6d93@newsspool2.arcor-online.net> <14p8llstxrtci$.18hb93fkpteuv$.dlg@40tude.net> <4ecd0652$0$6582$9b4e6d93@newsspool3.arcor-online.net> <1wyybnjde2yxq.1w37r5182t0xt.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 1322121015 22535 141.54.178.228 (24 Nov 2011 07:50:15 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Thu, 24 Nov 2011 07:50:15 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <1wyybnjde2yxq.1w37r5182t0xt.dlg@40tude.net> Xref: news2.google.com comp.lang.ada:14589 Content-Type: TEXT/PLAIN; charset=US-ASCII Date: 2011-11-24T08:46:33+01:00 List-Id: On Wed, 23 Nov 2011, Dmitry A. Kazakov wrote: > That is exactly why contracts cannot be dynamic. Dynamic means statically > undecidable. That point seems to be the main issue that makes this discussion going on and on ... Dynamic means it has not been statically decided by an apprpriate tool (such as SPARK). Good contracts are statically decidable! I guess, few c.l.a. people will disagree and claim that good contracts are statically undecidable. Now, if we have the tools to statically verify these contracts, then we are done. There is SPARK, but that very severely constrains Ada to be able to find proofs. Perhaps, within some time, there will be tools to statically verify some Ada 2012 contracts (google for HiLite Ada). In the meantime, Ada 2012 contracts are just claims made by the programmer (perhaps formally verified by hand or so). At this stage, what can you do? a) Documentation only -- the existence of the contract has no influence on the compiled code. b) Support for testing -- check the conditions during testing time, but turn to (a) after testing has been done. (*) c) Organized panic -- write the event into a log file; if neccessary, try to minimize the damage (e.g., write important data that has recently been changed into a temporary file); shut down. Ada 2012 supports all thee strategies (by using compiler switches), depending on the programmers' (or project mangagers') views and requirements. What should be wrong with this choice? And sure, Ada 2012 seems to allow you to write really lousy contracts, less than useful, with side-effects and whatever. To some degree, with pre => ..., post => ... is a bit like UNCHECKED_Something: useful when used with care, but dangerous. --------- (*) This is what someone denoted as "debugging" support. I think, testing is the better notion here. -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- ------ I love the taste of Cryptanalysis in the morning! ------