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 ry3mr13207509pbc.8.1340721673135; Tue, 26 Jun 2012 07:41:13 -0700 (PDT) Path: l9ni22294pbj.0!nntp.google.com!news2.google.com!goblin3!goblin.stu.neva.ru!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: about the new Ada 2012 pre/post conditions Date: Tue, 26 Jun 2012 16:54:45 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <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> <1i1mp8xs3vtl2.1oc4m66qtfgzq.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 1340721672 20646 141.54.178.228 (26 Jun 2012 14:41:12 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Tue, 26 Jun 2012 14:41:12 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: Content-Type: TEXT/PLAIN; charset=US-ASCII Date: 2012-06-26T16:54:45+02:00 List-Id: On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote: > On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote: > > Don't do that! Emit your messages to to the log file and then terminate! > > Contract violation => terminate. Exceptional state => recover. Yes, exactly! > > But then, what is more important: > > > > - Provide tools that support good software engineering practice? > > > > or > > > > - Prohibit any tools that can be misused? > > > > Dynamically checked contracts are such a tool. > > A wrench sold as shoe polish. This is my point! A wrench is good when used as a wrench, also quite good as a tool for cryptanalysis , but bad when misused as a shoe polish. > > And (I am sure you know this) any approach to really prove upper bounds > > on the storage requirements would imply to solve the Halting Problem. > > No problem. If you cannot prove it, that is compile error. It is a > conservative estimation, estimations have no halting problem issue, Boolean > values are bounded. > > The real problem lies elsewhere. Prover to tell program legality is thin > ice. Depending on the technique used the same program could be legal (good > prover) or illegal (poor prover). I don't know how to address this, though > nobody cares anyway... It is even worse! An Ada program is either legal or not. It would be a fatal mistake to make legality depend on the theorem prover one is using. That is precisely the reason for checked contracts: Within the language, we cannot prove them. With additional tools, we may be able to prove at least some of them. The tools will improve over time -- hopefully faster than new Ada standards arrive. In the mean time, we can do our best to figure out contract violations by testing. That means, dynamic checks in the test cases. > >> We certainly could learn from Java mistakes rather than repeating them > >> (e.g. interfaces). > > > > Which is probably why Ada so far has no contracted exceptions. Not that > > they cannot be done -- but nobody knows how to write such contracts that > > they really become useful. > > Huh, they didn't much hesitate to borrow flawed Java interfaces, although > the language already had abstract types. Yes, indeed. With respect to borrowing ideas from Java, the ARG has learned! -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- ------ I love the taste of Cryptanalysis in the morning! ------