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,c39ad3e35a7690a9 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Received: by 10.68.238.198 with SMTP id vm6mr12686000pbc.3.1329697269586; Sun, 19 Feb 2012 16:21:09 -0800 (PST) Path: wr5ni45424pbc.0!nntp.google.com!news2.google.com!postnews.google.com!o6g2000vbz.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Convention for naming of anything Date: Sun, 19 Feb 2012 16:21:09 -0800 (PST) Organization: http://groups.google.com Message-ID: <0b006973-6380-4328-a786-3a1283489bdc@o6g2000vbz.googlegroups.com> References: <6eb22e0f-bb55-4d03-8b63-f6a6c248e295@m24g2000yqb.googlegroups.com> NNTP-Posting-Host: 2.24.11.43 Mime-Version: 1.0 X-Trace: posting.google.com 1329697269 4829 127.0.0.1 (20 Feb 2012 00:21:09 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 20 Feb 2012 00:21:09 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: o6g2000vbz.googlegroups.com; posting-host=2.24.11.43; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: HUALENKRC X-HTTP-UserAgent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0) Gecko/20100101 Firefox/10.0,gzip(gfe) Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Date: 2012-02-19T16:21:09-08:00 List-Id: On Feb 19, 9:53=C2=A0pm, Yannick Duch=C3=AAne (Hibou57) wrote: > 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 > > =C2=A0 X =3D X=E2=82=80 + 1 > > says that the value of X is increased by 1. =C2=A0Perhaps an ASCII > > equivalent would be > > =C2=A0 X =3D X_0 + 1 > > Prior side note: I=E2=80=99ve checked GNAT reject it, the =E2=82=80, with= a message > =E2=80=9Cinvalid wide character in identifier=E2=80=9D, and this time, th= at'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 subprogra= m 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 alte= rnatives 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. For before and after values, perhaps X_Old and X is worth considering - then a postcondition e.g. X =3D X_Old + 1 would look more like it would for a program with a destructive update of X: X =3D X'Old + 1 > >http://www.cs.ox.ac.uk/publications/books/PfS/ > > [=E2=80=A6] > > I've come across exactly this conflict with primes in the past. =C2=A0T= he > > Ada verification tool, DAZ - built on ProofPower, see > >http://www.lemma-one.com/ProofPower/index/ > > Cool links, especially the former :-) Thanks I don't know of anyone who actually derives programs for real as described in PfS, but understanding the formal program development methods helps one justify or explain a program - not necessarily a formal argument but perhaps just better comments or more useful pre/ postconditions for run-time checking. The DAZ tool checks PfS-style refinement arguments. For example =F0=9D=9A=AB X [ true, X =3D X=E2=82=80 + 1 ] =E2=8A=91 X :=3D X + 1; would produce a verification condition, which, if provable means that the code is a valid implementation of the specification statement. As far as I know, DAZ was never used to develop programs (as described in PfS) but to check already written programs against a specification by 'recovering' a refinement that gave provable verification conditions. Then, verification conditions are shown to be provable by proving them - the subject of theorem proving is yet another (fascinating) world. Use of such tools tends to be limited to very critical systems. In fact, the analysis is very similar to compliance analysis with the SPARK examiner, though the presentation is very different. Phil