From: Vinzent Hoefler <ada.rocks@jlfencey.com>
Subject: Re: [Spark] Using defered constants
Date: Wed, 16 Apr 2003 11:27:13 -0400
Date: 2003-04-16T11:27:13-04:00 [thread overview]
Message-ID: <b7jsot$1mc1e$1@ID-175126.news.dfncis.de> (raw)
In-Reply-To: 1050505512.114638@master.nyc.kbcfp.com
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.
next prev parent reply other threads:[~2003-04-16 15:27 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-04-15 13:18 [Spark] Using defered constants Lutz Donnerhacke
2003-04-16 13:01 ` Rod Chapman
2003-04-16 13:37 ` Lutz Donnerhacke
2003-04-16 15:05 ` Hyman Rosen
2003-04-16 15:15 ` Lutz Donnerhacke
2003-04-16 15:27 ` Vinzent Hoefler [this message]
2003-04-23 9:28 ` Peter Amey
2003-04-23 10:52 ` Lutz Donnerhacke
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox