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
!summary
Annotations are provided to describe the use of global objects by subprograms.
!problem
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.
!proposal
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.
!wording
** TBD.
!discussion
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.
!example
!ASIS
** TBD.
!ACATS test
ACATS tests should be created to test that the new annotations are
correctly enforced.
!appendix
****************************************************************
Questions? Ask the ACAA Technical Agent