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-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,c8d893e8045967db
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-04-16 08:27:26 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!fu-berlin.de!uni-berlin.de!firewall.mdc-dayton.COM!not-for-mail
From: Vinzent Hoefler <ada.rocks@jlfencey.com>
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Using defered constants
Date: Wed, 16 Apr 2003 11:27:13 -0400
Organization: JeLlyFish software
Message-ID: <b7jsot$1mc1e$1@ID-175126.news.dfncis.de>
References: <slrnb9o1ke.oo.lutz@taranis.iks-jena.de>
 <cf2c6063.0304160501.62dcbd9d@posting.google.com>
 <slrnb9qn43.12t.lutz@taranis.iks-jena.de>
 <1050505512.114638@master.nyc.kbcfp.com>
NNTP-Posting-Host: firewall.mdc-dayton.com (12.161.103.180)
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: quoted-printable
X-Trace: fu-berlin.de 1050506845 1781806 12.161.103.180 (16 [175126])
X-Newsreader: Forte Agent 1.8/32.548
Xref: archiver1.google.com comp.lang.ada:36189
Date: 2003-04-16T11:27:13-04:00
List-Id: <comp.lang.ada>

Hyman Rosen <hyrosen@mail.com> wrote:

>Lutz Donnerhacke wrote:
>> It's an example. I need an access type there.
>
>SPARK doesn't have access types, I hear. I'm told
>that this is so that the correctness of the code
>is easier to prove,

Yes.

>and that code that needs access
>types should be written in plain Ada.

"SPARK 95 - The SPADE Ada 95 Kernel" explicitely states:

|Any Ada feature which does not appear in SPARK can still be employed
|if the subprogram which makes use of it has its body hidden by means
|of a "hide" directive ...

So I guess that is exactly what the #hide is intended for.

Lutz simply tries to use as much SPARK as possible. I do not think,
there is anything wrong with that approach.


Vinzent.