Version 1.1 of acs/ac-00324.txt

!standard 13.12.1(1.1/3) 20-01-31 AC95-00324/00
!standard 13.12.1(3/2)
!class Amendment 20-01-31
!status received no action 20-01-31
!status received 19-12-02
!subject SPARK unable to work under No_Implementation_Aspect_Specifications & No_Implementation_Pragmas restrictions

topic SPARK unable to work under No_Implementation_Aspect_Specifications & No_Implementation_Pragmas restrictions.

Currently, the usage of SPARK in conjunction with the Pragma Restrictions ( No_Implementation_Aspect_Specifications ) and Restrictions( No_Implementation_Pragmas ) is impossible because the SPARK_Mode pragma/aspect is not language-defined.

In order to fix this, we could have the SPARK_Mode aspect language-defined with the following values: Off, Thru_Public, Thru_Private, Thru_Body, Full -- leaving On as an implementation-value.

The reasoning for these multiple values coorespond to the current usage-rules of where "pragma SPARK_Mode(Off)" may appear and the effect it has.

In terms of packages, the values and their meanings are listed below:

Thru_Public: the visible-specification only is in SPARK; this cooresponds to the pragma Spark_Mode(Off) appearing immedately after the private keword in the specification.

Thru_Private: the entire specification is in SPARK; this cooresponds to either the pragma SPARK_Mode(Off) appearing immidately after the body [...] is construct, or the usage of the SPARK_Mode => Off aspect in the package-body. Thru_Body: the entire specification and body are in SPARK, excepting the initalization in the body; this cooresponds to the placement of pragma SPARK_Mode (Off) immidately before the begin keyword. Full: Cooresponds to pragma SPARK_Mode(On) in both the specification and body with no SPARK_Mode(Off) concerning that scope.

The only problem I see in this is that of complation-units which are not packages, and therefore do not have the same terminology; they do, however have much of the same concepts, and thus these values could be interpreted as:

Thru_Public: the subprogram's specification is in SPARK, but the implementation is not. Thru_Private: the subprogram's specification and declarative region are in SPARK but the region between begin and end is not. Thru_Body, Full: the entire subprogram is in SPARK.

Including the SPARK-Mode aspect as language defined, with these values, will then (a) allow the usage of SPARK in conjunction with the No_Implementation_Aspect_Specifications & No_Implementation_Pragmas restrictions; and (b) offer a greater degree of granularity/specificity in a single place than the current pragma SPARK_Mode ON/OFF values with restrictions on its placement.

***************************************************************

Though there is a general desire to keep SPARK a strict subset, it's not likely that SPARK will be (or should be) merged into the Ada standard. For that reason, SPARK_Mode is, by definition, an implementation-defined pragma. And so the Restrictions identifier No_Implementation_Pragmas and No_Implementation_Aspects should not allow SPARK_Mode.

I'm not convinced that this kind of change is worth it, since user having to forgo these restrictions for units implementing SPARK is a small price to pay. These kinds of restrictions are, IMO, rare enough (and deliberate enough) that this particular issue is not very serious.

***************************************************************

> Off, Thru_Public, Thru_Private, Thru_Body, Full

***************************************************************

Any compiler that supports SPARK could provide an implementation-defined restriction that disallows implementation-aspects and implementation-pragmas that are not "standard" SPARK and not standard Ada. That would probably be a better solution for SPARK users like you who want to avoid using "non-portable" features while still using SPARK.

Perhaps "No_Non_SPARK_Implementation_Aspects" and "No_Non_SPARK_Implementation_Pragmas".

***************************************************************

> Though there is a general desire to keep SPARK a strict subset, it's not > likely that SPARK will be (or should be) merged into the Ada standard. For > that reason, SPARK_Mode is, by definition, an implementation-defined pragma. > And so the Restrictions identifier No_Implementation_Pragmas and > No_Implementation_Aspects should not allow SPARK_Mode.

This is exactly why this should language-defined: to make using SPARK a proper subset.

***************************************************************

In that case, wouldn't it be better to just define SPARK_Mode in the Ada standard?

***************************************************************

I was transcribing it from one of those little notebooks I'd jotted ideas on.

***************************************************************

> This is exactly why this should language-defined: to make using SPARK a proper > subset.

I think AdaCore is reluctant to subject SPARK to the ISO standardization process at this point. Maybe some day...

***************************************************************

>Any compiler that supports SPARK could provide an >implementation-defined restriction that disallows >implementation-aspects and implementation-pragmas >that are not "standard" SPARK and not standard Ada. That would >probably be

>a better solution for SPARK users like you who want to avoid using >"non-portable" features while still using SPARK. > >Perhaps "No_Non_SPARK_Implementation_Aspects" and >"No_Non_SPARK_Implementation_Pragmas".

This seems like a better solution than standardizing parts of SPARK. It's hard to imagine that we could usefully standardize all of the SPARK-specific aspects and pragmas, and without that, it doesn't seem useful to standardize just a few of them (leaving the others to still be rejected by the pragmas).

I believe it is best to think of SPARK as a separate programming language (obviously one that is based on Ada and thus closely related to it). Attempting too hard to keep the languages the same is likely to stunt the evolution of both. The goals of the two languages are rather different (especially in terms of how errors are detected), and requiring the same solutions for both is likely to compromise both. Ada needs to be able to add new kinds of contracts and checks (both static and dynamic) without worrying about whether SPARK is trying to solve a similar but necessarily narrower problem. And SPARK should be able to add new kinds of types and statements without worrying about whether such things make sense in the richer environment of Ada.

(Note that I'm not suggesting that we make them different for the sake of doing that, just that the goals of the languages are different enough that forcing them to be the same in every case is likely to harm both.)

>This is exactly why this should language-defined: to make using SPARK a >proper subset.

This is definitely not a relevant goal for Ada, and I'd argue that it is not necessarily a long-term goal for SPARK, either. Even if it is a goal for SPARK today, things change and it may not be a goal for SPARK in the future. And the Ada Standard would be stuck with it forever, even if it is no longer relevant.

It might make sense for an Ada implementation to accept both Ada and SPARK code, but that sort of business decision doesn't involve the Ada Standard, but rather the demands of one's customers.

***************************************************************

>> Perhaps "No_Non_SPARK_Implementation_Aspects" and >> "No_Non_SPARK_Implementation_Pragmas". > > This seems like a better solution than standardizing parts of SPARK. > It's hard to imagine that we could usefully standardize all of the > SPARK-specific aspects and pragmas, and without that, it doesn't seem > useful to standardize just a few of them (leaving the others to still be > rejected by the pragmas).