## Types

The following data types have been built into the AGREE language:

Primitive Types: real, bool, int, and enumeration types (as described in Enumeration Types.

Composite Types: Record Types (as described in Record Expressions).

In addition, AGREE reasons about AADL features of the following types from the "Base_Types" package included in the AADL Plugin Resources library:

1. Base_Types::Boolean

2. Base_Types::Integer

   1. Base_Types::Integer_8

   2. Base_Types::Integer_16

   3. Base_Types::Integer_32

   4. Base_Types::Integer_64

   5. Base_Types::Unsigned_8

   6. Base_Types::Unsigned_16

   7. Base_Types::Unsigned_32

   8. Base_Types::Unsigned_64

3. Base_Types::Float

   1. Base_Types::Float_32

   2. Base_Types::Float_64

Note: Currently all bit-sized integer and unsigned types are approximated by unbound integers in AGREE. Similarly, all floating point numbers are approximated by rational numbers. More precisely, Base_Types::Boolean is mapped to the AGREE primitive type 'bool,' the various sizes of integer and unsigned types in Base_Types are mapped to the AGREE primitive type 'int,' and the floating point types in Base_Types are mapped to the AGREE primitive type 'real.' This means that AGREE results are not guaranteed to be sound with respect to system implementations that use bit-level representations. We expect that future versions of JKind will support bit-level integers, as these are widely supported by solvers. On the other hand, floating point solvers are currently immature, so it is likely that reals will be used for the foreseeable future. If exact floating point behavior (including rounding and truncation) are important to your verification problem, AGREE may provide incorrect answers.

AGREE reasons about AADL Data Implementations like record types. Consider the following example from a model of a medical device:

    data Alarm_Outputs
    end Alarm_Outputs;

    data implementation Alarm_Outputs.Impl
        subcomponents
            Is_Audio_Disabled : data Base_Types::Boolean;
            Notification_Message : data Base_Types::Integer;
            Log_Message_ID : data Base_Types::Integer;
    end Alarm_Outputs.Impl;

One can reference the fields of a variable of type Alarm_Outputs.Impl by placing a dot after the variable:

    Alarm.Is_Audio_Disabled => Alarm.Log_Message_ID > 3;

### Enumeration Types

Enumeration types may be specified either directly in AGREE annexes or specified in AADL. An AADL enumeration type is specified in the AADL data model by associating the property value `Enum` to the `Data_Representation` property and a property value list of enumerator strings to the `Enumerators` property. For example:

    data Primary_Color
        properties
            Data_Model::Data_Representation => Enum;
            Data_Model::Enumerators => ("Red", "Green", "Blue");
    end Primary_Color;

    data Pixel
    end Pixel;

    data implementation Pixel.Impl
        subcomponents
            color : data Primary_Color;
            x_pos : data Base_Types::Integer;
            y_pos : data Base_Types::Integer;
    end Pixel.Impl;

In AGREE annexes enumeration types may be defined using the keyword `enum` and a comma-separated list of enumerator identifiers. For example:

    enum card_suit = { spade, heart, club, diamond };

    eq color : card_suit;