Next: , Previous: , Up: Implementation Defined Aspects   [Contents][Index]


3.45 Aspect SPARK_Mode

This aspect is equivalent to pragma SPARK_Mode and may be specified for either or both of the specification and body of a subprogram or package.