Version 1.1 of ai12s/ai12-0079-2.txt

Unformatted version of ai12s/ai12-0079-2.txt version 1.1
Other versions for file 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
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 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.
** 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.
** TBD.
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.
** TBD.
** TBD.
!ACATS test
ACATS tests should be created to test that the new annotations are correctly enforced.


Questions? Ask the ACAA Technical Agent