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.220.230 with SMTP id pz6mr17014250pbc.3.1340723640796; Tue, 26 Jun 2012 08:14:00 -0700 (PDT) Path: l9ni22368pbj.0!nntp.google.com!news2.google.com!goblin3!goblin.stu.neva.ru!usenet.pasdenom.info!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: Tue, 26 Jun 2012 17:14:03 +0200 Organization: cbb software GmbH Message-ID: <16w5iwxhdmhe2.1h6wskrrrdjbc.dlg@40tude.net> 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: 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-26T17:14:03+02:00 List-Id: On Tue, 26 Jun 2012 16:54:45 +0200, stefan-lucks@see-the.signature wrote: > On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote: > >> 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 is an old problem. Not every legal program is compilable: X : constant := 2**(2**); > It would be a > fatal mistake to make legality depend on the theorem prover one is using. You cannot avoid this. The problem is to find right balance by moving most variations out of the sensitive area. > 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. I don't believe in tools. A full integration of the prover would open a completely new level of engineering, when amount of static checks could be adjusted by the programmer incrementally as the project matures by adding or removing goals to prove. >>>> 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! Nope, they just switched to Eiffel. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de