The idea here was that the specification of a subprogram
should have annotations indicating the global objects that it might manipulate.
For example a function can have side effects on global variables but
this important matter is not mentioned in the specification. This topic
has strong synergy with the information given in contracts such as pre-
and postconditions. However, it was abandoned perhaps because of the
complexity arising from the richness of the full Ada language. It should
be noted that such annotations have always featured in SPARK as comments
and moreover, at the time of writing, are being considered using the
aspect notation in a new version of SPARK. (See
AI-186).
© 2011, 2012, 2013 John Barnes Informatics.
