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,UTF8 Received: by 10.68.211.136 with SMTP id nc8mr8777341pbc.6.1335612690380; Sat, 28 Apr 2012 04:31:30 -0700 (PDT) Path: r9ni108010pbh.0!nntp.google.com!news2.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail From: phil.clayton@lineone.net Newsgroups: comp.lang.ada Subject: Re: Quantified expressions: no support for restriction predicates Date: Sat, 28 Apr 2012 04:30:00 -0700 (PDT) Organization: http://groups.google.com Message-ID: <796413.773.1335612600942.JavaMail.geo-discussion-forums@vbai3> References: <22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8> NNTP-Posting-Host: 2.24.14.131 Mime-Version: 1.0 X-Trace: posting.google.com 1335612690 30614 127.0.0.1 (28 Apr 2012 11:31:30 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 28 Apr 2012 11:31:30 +0000 (UTC) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=2.24.14.131; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Date: 2012-04-28T04:30:00-07:00 List-Id: On Saturday, April 28, 2012 12:43:51 AM UTC+1, Randy Brukardt wrote: > wrote in message=20 > news:22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8... > ... > >I can see the lack of restriction predicates being a potential 'gotcha'= =20 > >when writing/transforming > > pre/postconditions, e.g. incorrectly converting > > > > not (for all X in T =3D> if Odd(X) then P(X)) > > > >into > > > > (for some X in T =3D> if Odd(X) then not P(X)) >=20 > This is not a problem, since both of these are illegal. :-) Conditional= =20 > expressions always have to be directly enclosed in parens, and that isn't= =20 > done here. (There are special cases to allow the omission of those parens= =20 > when they are already *directly* there, but in only those cases, like P(i= f=20 > Odd(X) then not P(X)); but not P(Param =3D> if Odd(X) then not P(X));.) >=20 > Has nothing to do with your point, though. Drat. I knew about the parentheses. (Personally, I would have liked paren= theses to be required only when there is a syntactic ambiguity. I suppose = that is so often, you may as well have them all the time.) > ... > >I haven't followed all the developments in the areas of predicates.=20 > >Perhaps there are good reasons > > not to have such restriction predicates. Anyway, just thought I would= =20 > > raise the idea as they seem useful. >=20 > We decided to leave all of the contract expressions as code easily=20 > understandable by any novice Ada programmer (or middle-aged Ada programme= r=20 > who has forgotten most of the advanced mathematics he once knew - like, s= ay,=20 > me :-). >=20 > Conditional expressions and quantified expressions themselves were both a= =20 > bit controversial for this reason. We added conditional expressions mainl= y=20 > so that implications and the like could be specified without having to wr= ite=20 > a separate function (which of course would defy compile-time analysis as = the=20 > body wouldn't be present). We rejected the idea of an "implies" operator= =20 > because a lot of people are confused by what it means -- the equivalent= =20 > conditional expression is much clearer, especially at 2 am! I think "if P then Q", i.e. implicit "else true", is a really neat way to p= rovide implies. It will be much more widely understood than an implies ope= rator and makes clear when Q is evaluated. > Quantified expressions are hard enough to understand as it is. I don't th= ink=20 > complicating them further would be helpful, especially for the programmer= =20 > that only saw them rarely (which is likely to be most Ada programmers). Honestly, my motivation was to help those who were a little rusty on their = maths/logic! May be I wrote one to many =E2=88=80s :) My thinking is that having a predicate to restrict the elements that one is= quantifying over (just like a subtype predicate restricts the elements of = a subtype) would avoid the need to work out the equivalent logical expressi= on, which differs depending on the quantifier - a likely source of error. = So, while more syntax would be needed, this should actually simplify quanti= fication concepts. It's all a bit late in the day anyway but I feel better now I've said that! Phil