SPARK constants across packages

SPARK constants across packages

[xorquewasp]

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?

Re: SPARK constants across packages

[Phil Thornley]

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

Re: SPARK constants across packages

[xorquewasp]

Phil Thornley wrote:
> 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".

Oh, right.

> 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."

Thanks.

Perhaps SPARK 05 might stretch to allowing this when the source
value is in a Pure package.

Perhaps not.