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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,802ee425bbc3eba3 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.204.157.134 with SMTP id b6mr649480bkx.5.1335570240558; Fri, 27 Apr 2012 16:44:00 -0700 (PDT) MIME-Version: 1.0 Path: h15ni173206bkw.0!nntp.google.com!news2.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.newsland.it!newsfeed.x-privat.org!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Quantified expressions: no support for restriction predicates Date: Fri, 27 Apr 2012 18:43:51 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1335570237 16239 69.95.181.76 (27 Apr 2012 23:43:57 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 27 Apr 2012 23:43:57 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-04-27T18:43:51-05:00 List-Id: wrote in message news:22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8... ... >I can see the lack of restriction predicates being a potential 'gotcha' >when writing/transforming > pre/postconditions, e.g. incorrectly converting > > not (for all X in T => if Odd(X) then P(X)) > >into > > (for some X in T => if Odd(X) then not P(X)) This is not a problem, since both of these are illegal. :-) Conditional expressions always have to be directly enclosed in parens, and that isn't done here. (There are special cases to allow the omission of those parens when they are already *directly* there, but in only those cases, like P(if Odd(X) then not P(X)); but not P(Param => if Odd(X) then not P(X));.) Has nothing to do with your point, though. ... >I haven't followed all the developments in the areas of predicates. >Perhaps there are good reasons > not to have such restriction predicates. Anyway, just thought I would > raise the idea as they seem useful. We decided to leave all of the contract expressions as code easily understandable by any novice Ada programmer (or middle-aged Ada programmer who has forgotten most of the advanced mathematics he once knew - like, say, me :-). Conditional expressions and quantified expressions themselves were both a bit controversial for this reason. We added conditional expressions mainly so that implications and the like could be specified without having to write a separate function (which of course would defy compile-time analysis as the body wouldn't be present). We rejected the idea of an "implies" operator because a lot of people are confused by what it means -- the equivalent conditional expression is much clearer, especially at 2 am! Quantified expressions are hard enough to understand as it is. I don't think complicating them further would be helpful, especially for the programmer that only saw them rarely (which is likely to be most Ada programmers). Randy.