Re: [SPARK] Code safety and information hiding

["Jeffrey R. Carter" <spam.not.jrcarter@acm.not.spam.org>]

Peter Amey wrote:
> 
> 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).

To my mind, in a well designed system, all the "global" variables will 
be state variables, and I'd prefer to reserve the term "global" for 
package-spec variables.

> 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!

I think it would be better if you'd educated your customer on how to use 
that better solution, and kept SPARK as it was.

Interesting that my aside on my personal preference for terminology has 
generated so much traffic.

-- 
Jeff Carter
"Brave Sir Robin ran away."
Monty Python and the Holy Grail
59