Next: Aspect No_Caching, Previous: Aspect Max_Queue_Length, Up: Implementation Defined Aspects [Contents][Index]
For the syntax and semantics of this aspect, see the SPARK 2014 Reference Manual, section TBD.