Annotated King Reference Manual/Types

This page is work in progress.

Type Declarations

Some general principles:

• All scalar subtypes have a default value. For bounded numeric and enumeration subtypes, this is the 'First of the subtype, unless a different value is specified with the Default_Value aspect. For unbounded numeric subtypes, the Default_Value aspect must be specified. Note that an unbounded numeric type can have bounded subtypes.
• The Predicate aspect may be specified for all subtypes.
• All scalar types have the attributes 'Image, 'Value, 'Min, 'Max, 'Previous, and 'Next.
• Integer and enumeration types have the attributes 'Position, 'Value (integer), 'Representation, and 'From_Representation. For integer types, 'Position and 'Representation both give the value of the parameter, and 'Value (integer) and 'From_Representation give the value of the type with the value of the parameter (if that exists); this is similar to 'Pos and "Val for integer types in Ada.
• 'Image <=>, 'Value (string) are inverses of each other, as are 'Position <=> 'Value (integer)

Syntax

type_declaration ::= full_type_declaration | hidden_type_declaration

full_type_declaration ::=
          type defining_identifier [known_discriminant_part] is type_definition
             [aspect_specification];

hidden_type_declaration ::=
          type defining_identifier [discriminant_part] is hidden
             [aspect_specification];

discriminant_part ::= unknown_discriminant_part | known_discriminant_part

unknown_discriminant_part ::= (<>)

known_discriminant_part ::= (discriminant_specification {; discriminant_specification})

discriminant_specification ::=
          defining_identifier : subtype_mark [<- default_expression]  

type_definition ::=
            enumeration_type_definition
          | integer_type_definition
          | real_type_definition
          | map_type_definition
          | sequence_type_definition
          | set_type_definition
          | record_type_definition
          | derived_type_definition
          | module_type_definition
          | task_type_definition

Rationale

-

Discussion

-

Enumeration Types

Examples

type Suit is (Spade, Club, Heart, Diamond);

type Philosopher_ID is (Archimedes, Descartes, Hegel, Kant, Socrates);

Syntax

enumeration_type_definition ::=
         (enumeration_literal_specification {, enumeration_literal_specification})

enumeration_literal_specification ::= defining_identifier | defining_character_literal

Operators

= /= < <= > >=

Attributes

First, Last, Position, From_Representation, Representation, Image, Value, Min, Max, Previous, Next

Aspects

Bit_Size, Byte_Size

Object declaration

My_Card : Suit;

Rationale

-

Discussion

-

Integer Types

Examples

Bounded integer types

type Day is range 1 .. 31;

Unbounded integer types

type Factorial is range <> with Default_Value => 0;

Syntax

integer_type_definition ::= bounded_integer_type_definition | unbounded_integer_type_definition

bounded_integer_type_definition ::= range static_simple_expression .. static_simple_expression

unbounded_integer_type_definition ::= range <>

Operators

+ - * / rem mod ^ = /= < <= > >= and or xor not

Attributes

First, Last, Bit_Wise_Operators, Image, Value, Min, Max, Previous, Next, Valid

Additional attributes with Bit_Wise_Operators = True:

Shift_Left, Shift_Right, Rotate_Left, Rotate_Right, Mod

Aspects

Default_Value, Predicate, Signed_Representation, Overflow_Checking

Object declaration

N : Factorial;

Rationale

Bit-wise operations are available for the base type of all bounded integer types that fit in a single hardware integer.

Discussion

-

Real Types

Syntax

real_type_definition ::= floating_point_definition | fixed_point_definition

Floating Point Types

Examples

Bounded floating-Point Types

type Risk is digits 7 range 0 .. 1;

Unbounded floating-Point Types

type Rational is digits <> with Default_Value => 0;

Syntax

floating_point_definition ::=
          bounded_floating_point_definition | unbounded_floating_point_definition

bounded_floating_point_definition ::= digits static_expression [real_range_specification]

real_range_specification ::= range static_simple_expression .. static_simple_expression

unbounded_floating_point_definition ::= digits <>

Operators

+ - * / ^ = /= < <= > >=

Attributes

Image, Value, Min, Max, Previous, Next, Valid, digits

Aspects

Default_Value, Predicate

Object declaration

Speed : Rational;

Rationale

-

Discussion

-

Fixed Point Types

Examples

Bounded fixed-Point Types

type Angle is delta 0.01 range -3.14 .. 3.14;

Unbounded fixed-Point Types

type Duration is delta 10.0 ^ -9 range <> with Default_Value => 0;

Syntax

fixed_point_definition ::= bounded_fixed_point_definition | unbounded_fixed_point_definition

bounded_fixed_point_definition ::= delta static_expression real_range_specification

unbounded_fixed_point_definition ::= delta static_expression range <>

Operators

+ - * / ^ = /= < <= > >=

Attributes

Image, Value, Min, Max, Previous, Next, Valid, delta

Aspects

Default_Value, Predicate

Object declaration

Bearing : Angle;

Rationale

Shouldn't decimal types be available, in order to cover the corresponding available type of Ada?

A King fixed-point type with a delta that is a power of 10 is equivalent to an Ada decimal fixed-point type.

type Money is delta 0.01 digits 14;

The above would be equivalent to:

type Money is delta 0.01 range -999_999_999_999.99 .. 999_999_999_999.99;

Discussion

-

Map Types

Examples

type Store is map Part_Key => Stock_Info;

Syntax

map_type_definition := map key_subtype_mark => value_subtype_mark

Operators

= /=

"=" is only defined if it is defined for the value subtype.

Attributes

-

Operations

Delete, Clear, Defined, Size

Aspects

-

Object declaration

My_Store : Store;

Component deference

My_Store (K99)

Aggregates

Store'(K1 => SI1, KE => SIE)

Store'(null) -- Empty map

Iteration

for K in My_Store'range

for E of My_Store

Rationale

Maps may also be implemented by functions, so King uses a common notation for both.

Discussion

-

Sequence Types

Examples

type Stack is sequence of Message;

Syntax

sequence_type_definition := sequence of element_subtype_mark

Operators

= /= &

"=" is only defined if it is defined for the value subtype.

Attributes

-

Operations

Delete, Clear, Length

Aspects

-

Object declaration

My_Stack : Stack;

Component deference

My_Stack [Curent]

Aggregates

My_Stack'[MC, ML, MZ]

My_Stack'[null] -- Empty sequence

Iteration

for P in [reverse] My_Stack'range

for E of [reverse] My_Stack

Rationale

-

Discussion

-

Set Types

Examples

type File_Mask is set of File_Mode;

Syntax

set_type_definition := set of element_subtype_mark

Operators

+ - * / = /= < <= > >= [not] in

Attributes

-

Operations

Size

Aspects

-

Object declaration

My_Mask : File_Mask:

Component deference

-

Aggregates

My_Mask'{Read, Exec}

My_Mask'{null} -- Empty set

My_Mask'{all} -- Full set

Iteration

for M of My_Mask

Rationale

-

Discussion

-

Record Types

Examples

type Complex is record
   Re : Float;
   Im : Float;
end record Complex;

Syntax

record_type_definition ::= record_definition

record_definition ::=
           record
              component_list
           end record record_identifier

component_list ::=
            component_item {component_item}
          | {component_item} variant_part
          | null;

component_item ::= component_declaration

component_declaration ::= defining_identifier : component_definition [<- default_expression]
                          [aspect_specification];

component_definition ::= subtype_indication

variant_part ::= case discriminant_direct_name is
                   variant
                   {variant}
                 end case;

variant ::= when discrete_choice_list =>
               component_list

discrete_choice_list ::= discrete_choice {| discrete_choice}

discrete_choice ::= choice_expression | discrete_subtype_indication | range_specification | others

Operators

= /=

Attributes

-

Aspects

-

Object declaration

Z : Complex;

Component deference

Z.Re

Rationale

-

Discussion

-

Derived Types

Examples

type Boxes (Length : Position_Value) is record
   Box_A : Receive_Box (Max_Length => Length);
   Box_B : Receive_Box (Max_Length => Length);
end record;
type Boxes_4 is new Boxes (Length => 4);

Syntax

derived_type_definition ::= new parent_subtype_indication

Operators

-

Attributes

-

Aspects

-

Rationale

The operations, attributes, and so on are based on the parent type.

Discussion

-

Module Types

Examples

type Strings is module
   Set : procedure (S : String);
   Index : function (Pattern : String; Going : Direction <- Forward) return Position_Value;
   Head : function (Count : Natural; Pad : Unicode <- Space) return String;
   -- ...
end module Strings;

Syntax

module_type_definition ::= module
                              subprogram_declaration {subprogram_declaration}
                           end module module_identifier

Operators

-

Attributes

-

Aspects

-

Rationale

-

Discussion

-

Active Task Types

Examples

type Philosopher (ID : Philosopher_ID <- Archimedes) is task;

Syntax

task_type_definition ::= task

Operators

= /=

Attributes

-

Aspects

-

Object declaration

T1 : Philosopher;

Rationale

-

Discussion

-

Passive Task Types

Examples

type Semaphore is task
   Secure : procedure;
   Release : procedure;
end task Semaphore;

Syntax

task_type_definition ::= task
                            subprogram_declaration {subprogram_declaration}
                         end task task_identifier

Operators

= /=

Attributes

-

Aspects

-

Object declaration

S1 : Semaphore;

Rationale

Passive tasks are the only way that active tasks may communicate.

Discussion

-