Version 1.1 of ai12s/ai12-0079-2.txt
!standard 6.1.2(0) 19-10-05 AI12-0079-2/00
!class Amendment 19-10-05
!status work item 19-10-05
!status received 19-10-05
!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
requires 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
** TBD. Similar to AI12-0079-1 and it's later fixups (AI12-0240-6 [overriding],
AI12-0303-1, AI12-0310-1, and AI12-0334-2), but with some in the core
and some in an annex.
!wording
** TBD.
!discussion
Global annotations are critical to being able to perform any sort of modular
static analysis.
The intent is that all of the global in, in-out, and out annotations
proposed can be statically checked.
** Rest TBD.
!example
** TBD.
!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