From: Phil Thornley <phil.jpthornley@googlemail.com>
Subject: Re: SPARK constants across packages
Date: Sun, 7 Jun 2009 10:21:04 -0700 (PDT)
Date: 2009-06-07T10:21:04-07:00 [thread overview]
Message-ID: <270915f0-2b00-40ae-bf37-97c2796f1837@r3g2000vbp.googlegroups.com> (raw)
In-Reply-To: 07c4ba96-85c2-4588-a63a-6d61a27f2349@q16g2000yqg.googlegroups.com
On 7 June, 17:53, xorquew...@googlemail.com wrote:
> SPARK appears to forbid this:
>
> X : constant Integer := 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
next prev parent reply other threads:[~2009-06-07 17:21 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-07 16:53 SPARK constants across packages xorquewasp
2009-06-07 17:21 ` Phil Thornley [this message]
2009-06-07 17:34 ` xorquewasp
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox