Next: Annotate, Up: Implementation Defined Aspects
This aspect is equivalent to pragma Abstract_State.