Re: [SPARK] Code safety and information hiding

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Robert A Duff wrote:
> "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.

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