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

-