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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,6e5bbc32bcc6c91c
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!r3g2000vbp.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK constants across packages
Date: Sun, 7 Jun 2009 10:21:04 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <270915f0-2b00-40ae-bf37-97c2796f1837@r3g2000vbp.googlegroups.com>
References: 
 <07c4ba96-85c2-4588-a63a-6d61a27f2349@q16g2000yqg.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1244395264 9140 127.0.0.1 (7 Jun 2009 17:21:04
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sun, 7 Jun 2009 17:21:04 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: r3g2000vbp.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1;
	Trident/4.0; .NET CLR 1.1.4322; .NET CLR 2.0.50727),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6356
Date: 2009-06-07T10:21:04-07:00
List-Id: <comp.lang.ada>

On 7 June, 17:53, xorquew...@googlemail.com wrote:
> SPARK appears to forbid this:
>
> =A0 X : constant Integer :=3D P.Y;
>
> Where Y is a constant of the same type defined in package P;
> The grammar for SPARK 95 specifies that only a
> static_simple_expression can appear after the assignment
> operator for constant declarations.
>
> Is there a particular reason that SPARK doesn't allow this?

The place to look first for any "why does SPARK excluded this"
question is Section 4 of the SPARK95 manual - "Considerations in the
Refinement of the Ada Subset".

For this particular query the answer is (in 4.1) that the meaning of
the program must not be changed by different orders of elaboration.
"This particular problem is overcome in SPARK by the restrictions
imposed on ... initialization expressions."

Cheers,

Phil Thornley