Version 1.2 of ai12s/ai12-0079-1.txt

!standard 7.3.2(3/3) 13-06-28 AI12-0079-1/00
!class Amendment 13-06-28
!status work item 13-06-28
!status received 13-06-14
!priority High
!difficulty Hard
!subject Global-in and global-out annotations

Annotations are provided to describe the use of global objects by subprograms.

Ada 2012 added many kinds of assertions to Ada in order to increase the ability of a programmer to specify contracts for types and subprograms. These contracts are defined to be checked at runtime, but are intended to be potentially checked (at least in part) statically.

However, without knowledge of side-effects of functions used in the aspects, a tool has to assume the worst about any user-defined functions. For example, that the result of a function can change even when called with the same operands. Other assumptions could cause incorrect programs to be accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution. Both of these results are unacceptable for a feature intended to improve the correctness of programs.

The worst-case assumptions pretty much prevent any analysis unless the bodies of any user-defined functions used in the aspects are available. This is bad, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body require creating pseudo body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again); but the language does not allow these to be "real" body dependencies (any recompilation needed has to occur automatically).

Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side-effects is needed in the specification of subprograms in order to accomplish that goal.

Note that the "new" SPARK (currently in development) will include aspects to specify dependencies on globals by subprograms. These can form the root of a solution for Ada. They're not enough by themselves, as SPARK does not include dynamic memory allocation, so we need to add (at a minimum) support for dependence on storage pools to the SPARK mechanism.

[Editor's note: The above is all that I know at this point, June 2013. Hopefully, we'll have more information when we start working seriously on Ada 2020.]

We had a partially worked out proposal in AI05-0186-1, for types, packages, and subprograms. We considered that proposal too immature to use in Ada 2012, but at least some of the ideas it embodies could be useful.

The global in and global out annotations ought to be descriptive. That is, the annotations describe the behavior of the subprogram body, initialization/finalization of a type, or elaboration of a package. As such, these annotations should be checked. There is no benefit to be gained from lying about side-effects; such incorrect information could easily lead to incorrect code being generated (if the compiler uses the annotations). Moreover, if it is impractical to specify the correct annotations, it makes sense to specify none at all.

All of the global in and global out annotations proposed can be statically checked. It is possible to imagine annotations that cannot be statically checked, but these are assumptions as opposed to descriptive. Assumptions are a different set of annotations.

Note that it is possible to lie about the use of globals of subprograms and other entities that are imported. This is of course impossible to check, but thankfully is covered by B.1(38.1/2). Incorrect annotations on imported subprograms could cause a program to be erroneous.