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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,c39ad3e35a7690a9 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Received: by 10.68.74.201 with SMTP id w9mr12490667pbv.0.1329688388669; Sun, 19 Feb 2012 13:53:08 -0800 (PST) Path: wr5ni45022pbc.0!nntp.google.com!news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Convention for naming of anything Date: Sun, 19 Feb 2012 22:53:06 +0100 Organization: Ada @ Home Message-ID: References: <6eb22e0f-bb55-4d03-8b63-f6a6c248e295@m24g2000yqb.googlegroups.com> NNTP-Posting-Host: bpWizFDETHN8QGoKhhcP5g.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/11.61 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable Date: 2012-02-19T22:53:06+01:00 List-Id: Le Sun, 19 Feb 2012 19:07:15 +0100, Phil Clayton = a =C3=A9crit: > To refer to before and after values of a variable in e.g. a > postcondition, the convention of suffixing a subscript-zero to denote > the before value is fairly common in formal methods texts, e.g. the > classic "Programming from Specifications": > http://www.cs.ox.ac.uk/publications/books/PfS/ > So, for example, the postcondition > X =3D X=E2=82=80 + 1 > says that the value of X is increased by 1. Perhaps an ASCII > equivalent would be > X =3D X_0 + 1 Prior side note: I=E2=80=99ve checked GNAT reject it, the =E2=82=80, wit= h a message = =E2=80=9Cinvalid wide character in identifier=E2=80=9D, and this time, t= hat's not due to = missing compiler options. Will really need to check the RM for these = characters, so my comments may not not relevant. X=E2=82=80 or X_0 Could be an option if everything was formal in a given= = application. But when a specification is expected to be exposed with a = classic look, this would imply giving subprograms argument names like X=E2= =82=80 = or X_0, as the =E2=80=9Cvalue before=E2=80=9D is often from the subprogr= am parameters, and = this wouldn't look as expected. May be OK or not, depending on the overall style of an application. But you gave me the idea X=E2=82=81, X=E2=82=82, X=E2=82=83 could be alt= ernatives to X=CA=B9 or X=CB=8A, = more distinctive, except it may make readers think they are list indexes= = or polynomial indexes=E2=80=A6 Hint: =E2=82=80 is U+2080, =E2=82=81 is U+2081, and so on, up to =E2=82=89= . Use of a character = palette is probably recommended to help. > http://www.cs.ox.ac.uk/publications/books/PfS/ > [=E2=80=A6] > I've come across exactly this conflict with primes in the past. The > Ada verification tool, DAZ - built on ProofPower, see > http://www.lemma-one.com/ProofPower/index/ Cool links, especially the former :-) Thanks -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity