Annotated King Reference Manual/Aspects

Aspect Clauses Examples - Syntax aspect_clause ::= attribute_definition_clause attribute_definition_clause ::= for local_name'attribute_designator use expression; | for local_name'attribute_designator use name; local_name ::= direct_name | direct_name'attribute_designator | library_unit_name null_declaration ::= null; Rationale - Discussion - Aspect Specifications Examples Append : procedure (Onto : in out List; Item : in Element) with Precondition => not Onto.Is_Full, Postcondition => not Onto.Is_Empty and Onto.Value (Onto.Last) = Item; type Byte_Value is range 0 .. 255 with Signed_Representation => False; Syntax aspect_specification ::= with aspect_mark [=> aspect_definition] {, aspect_mark [=> aspect_definition]} aspect_mark ::= aspect_identifier aspect_definition ::= name | expression | identifier | aggregate | global_aspect_definition global_aspect_definition ::= null | Unspecified | global_mode global_designator | (global_aspect_element{; global_aspect_element}) global_aspect_element ::= global_mode global_set | global_mode all | global_mode Synchronized global_mode ::= basic_global_mode | extended_global_mode basic_global_mode ::= in | in out | out extended_global_mode ::= Overriding basic_global_mode global_set ::= global_name {, global_name} global_designator ::= all | Synchronized | global_name global_name ::= object_name | module_name Rationale - Discussion -