Re: [SPARK] Code safety and information hiding

[Robert A Duff <bobduff@shell01.TheWorld.com>]

"Jeffrey R. Carter" <spam.not.jrcarter@acm.not.spam.org> 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.

Jeff wants to consider package-spec variables particularly evil.
OK, but there are global variables even more global than that.
The Registry in windows is an obnoxiously global variable.
And environment variables under many operating systems are
obnoxiously global.  I suppose disk files are global, although
I don't usually find them obnoxious.

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).

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.

AARM-8.1 says:

14    [{local to} A declaration is local to a declarative region if the
declaration occurs immediately within the declarative region.] [An entity is
local to a declarative region if the entity is declared by a declaration that
is local to the declarative region.]

    14.a  Ramification: "Occurs immediately within" and "local to" are
          synonyms (when referring to declarations).

    14.b  Thus, "local to" applies to both declarations and entities, whereas
          "occurs immediately within" only applies to declarations. We use
          this term only informally; for cases where precision is required, we
          use the term "occurs immediately within", since it is less likely to
          cause confusion.

15    {global to} A declaration is global to a declarative region if the
declaration occurs immediately within another declarative region that encloses
the declarative region. An entity is global to a declarative region if the
entity is declared by a declaration that is global to the declarative region.

- Bob