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!border1.nntp.dca.giganews.com!nntp.giganews.com!wns14feed!worldnet.att.net!attbi_s22.POSTED!53ab2750!not-for-mail
From: "Jeffrey R. Carter" <spam.not.jrcarter@acm.not.spam.org>
Organization: jrcarter at acm dot org
User-Agent: Thunderbird 1.5.0.5 (Windows/20060719)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: [SPARK] Code safety and information hiding
References: <ebuj47$bal$1@sunnews.cern.ch> <gFKEg.138542$1i1.49988@attbi_s72>
 <wccoduhy7er.fsf@shell01.TheWorld.com> <4l2mcnFee3k7U1@individual.net>
In-Reply-To: <4l2mcnFee3k7U1@individual.net>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <CM4Hg.924538$084.512630@attbi_s22>
NNTP-Posting-Host: 12.201.97.176
X-Complaints-To: abuse@mchsi.com
X-Trace: attbi_s22 1156372642 12.201.97.176 (Wed, 23 Aug 2006 22:37:22 GMT)
NNTP-Posting-Date: Wed, 23 Aug 2006 22:37:22 GMT
Date: Wed, 23 Aug 2006 22:37:22 GMT
Xref: g2news2.google.com comp.lang.ada:6328
Date: 2006-08-23T22:37:22+00:00
List-Id: <comp.lang.ada>

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