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,34257fd17abeba14 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: [SPARK] Code safety and information hiding Date: Wed, 23 Aug 2006 10:44:54 +0100 Message-ID: <4l2mcnFee3k7U1@individual.net> References: Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net sqqCL8+Wa/fdZz+vY9rxIQpoy3GOfnJMPrcEW0KX6nFdXV78U= User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en In-Reply-To: Xref: g2news2.google.com comp.lang.ada:6323 Date: 2006-08-23T10:44:54+01:00 List-Id: Robert A Duff wrote: > "Jeffrey R. Carter" writes: > > >>[Aside: I really don't like the use of the term "global" for state >>variables. True global variables (in package specs) should be illegal; >>state variables are a different cup of fish and should not be tainted by >>the "global" label.] > > > I think the terms "global" and "local" are most useful if they are > relative to something. A variable can be more global or less global. > The Ada RM agrees with that (not surprising, since I wrote > that part ;-)). See quote below. That's certainly the design decision we made with SPARK. The term global is always relative to the place where you are asking the question. If an entity is declared outside the declarative part of the place from which you are looking it is global otherwise it is local. A local variable of a subprogram may well be a global to a nested subprogram for example. SPARK's global annotation eliminates "hole in scope" issues (as well as doing other useful things). [snip] > > I don't agree that package-spec variables should be illegal. Such a > rule accomplishes nothing, since the programmer can just have a getter > and a setter, which is just as evil. In some rare cases, a package-spec > variable makes sense, and in those cases, the getter/setter method is no > better (just more verbose). SPARK doesn't prohibit package-spec variables (actually it did in the very early days but a large and influential customer made us change our minds); however, it does nag you in various ways if you make use of them. Abstract own variables and refinement clauses are a much better solution! > > So I like the SPARK syntax for "global". It means so-and-so variable is > global to this procedure, not necessarily global to the whole program, > or global to that part of the program that with's certain package, or > global to the whole world. > Thanks! Peter