== Values A *value* is one of the following: * A primitive integer value * An integer value * A floating-point value * A Boolean value * A string value * An abstract type value * An anonymous array value * An array value * An enumeration value * An anonymous struct value * A struct value Every value _v_ belongs to exactly one <> _T_, except that every string value belongs to every string type. Every value that belongs to type _T_ also belongs to every <> whose <> is _T_. When a value _v_ belongs to a type _T_, we say that _v_ is a value *of type _T_*. In the following subsections, we describe each kind of value and its associated canonical types. === Primitive Integer Values A *primitive integer value* is an ordinary (mathematical) integer value together with its canonical type, which is a <>. Formally, the set of primitive integer values is the disjoint union over the integer types of the values represented by each type: * An unsigned integer type of width stem:[w] represents integers in the range stem:[[0, 2^w-1\]]. For example, `U8` represents the integers stem:[[0, 255\]]. * A signed integer type of width stem:[w] represents integers in the range stem:[[-2^(w-1), 2^(w-1)-1\]]. For example, `I8` represents the integers stem:[[-128, 127\]]. We represent a primitive integer value as an expression followed by a colon and a primitive integer type. For example, we write the value 1 at type `U32` as `1: U32`. The value `1: U32` is distinct from the value `1: U8`. === Integer Values An *integer value* is an ordinary (mathematical) integer value. Its canonical type is _Integer_. We represent an integer value as an integer number, with no explicit type. For example, `1` is an integer value. === Floating-Point Values A *floating-point value* is an IEEE floating-point value of 4- or 8-byte width. Formally, the set of floating-point values is the disjoint union over the types `F32` and `F64` of the values represented by each type: * The type `F32` represents all IEEE 4-byte floating-point values. * The type `F64` represents all IEEE 8-byte floating-point values. We write a floating-point values analogously to primitive integer values. For example, we write the value 1.0 at type `F32` as `1.0: F32`. The canonical type of a floating-point value is `F32` or `F64`. === Boolean Values A *Boolean value* is one of the values `true` and `false`. Its canonical type is `bool`. === String Values A *string value* is a sequence of characters that can be represented as a <>. It is written in the same way as a string literal expression, e.g., `"abc"`. Every string value _v_ has a *length*, which is the number of characters in the sequence. A string value _v_ belongs to every string type. Note that _v_ may have length _m_ and type `string size` _n_, with stem:[m > n]. In this case, the behavior is defined by the code generation strategy. In particular, when code is generated for the F Prime framework, the value _v_ may be stored into a buffer that can hold a maximum string length of _n_. If this happens, the framework will *truncate* the value _v_ to _n_ characters before storing it. That means that the first _n_ characters of _v_ are stored in the buffer. === Abstract Type Values An *abstract type value* is a value associated with an abstract type. For each abstract type stem:[T], there is one value with canonical type stem:[T]. This value is not represented explicitly in the model, but it may be represented in the generated code, e.g., as an object with default initialization. We write the value `value of type` stem:[T]. === Anonymous Array Values An *anonymous array value* is a value associated with an anonymous array type. We write an anonymous array value similarly to an <>: an anonymous array value stem:[v] has the form `[` stem:[v_1] `,` stem:[...] `,` stem:[v_{n-1}] `]`, where . stem:[n] is a positive integer called the *size* of the anonymous array value. . For each stem:[i in [0,n-1]], stem:[v_i] is a value of type stem:[T] for some <> stem:[T]. The canonical type of stem:[v] is _[_ stem:[n] _]_ stem:[T]. Note that for an anonymous array value stem:[v] to be well-formed, the member values must have identical types. If an array expression appearing in the source syntax has member values with non-identical types, then one or more members must be converted to a different type before forming stem:[v]. === Array Values An *array value* is a value associated with an array type. We write an array value like an <>, except that the value is annotated with an <>. An array value has the form `[` stem:[v_0] `,` stem:[...] `,` stem:[v_{n-1}] `]` `:` stem:[Q], where . stem:[n] is a positive integer called the *size* of the array value. . stem:[Q] is a <> that refers to a <> with member type stem:[T]. . For each stem:[i in [0,n-1]], stem:[v_i] is a value of type stem:[T]. Note that stem:[T] need not be a canonical type. For example, it is permissible for stem:[T] to be `T`, for `T` to be an alias of `U32`, and for stem:[v] to be the value `[ 0: U32, 1: U32 ]`. In this case `0: U32` and `1: U32` are values of type `T`, as required. The canonical type of the value is stem:[Q]. === Enumeration Values An *enumeration value* is a value associated with an <>. It is a pair consisting of the name and the integer value specified in the enumerated constant definition. Its canonical type is the type associated with the <> in which the enumerated constant definition appears. === Anonymous Struct Values An *anonymous struct value* is a value associated with an <>. We write an anonymous struct value stem:[v] similarly to a <>: a struct value has the form `{` stem:[m_1] `=` stem:[v_1] `,` stem:[...] `,` stem:[m_n] `=` stem:[v_n] `}`, where for each stem:[i in [1,n]], stem:[v_i] is a value of type stem:[T_i]. The elements stem:[m_i] `=` stem:[v_i] are called the *members* of the value. Each type stem:[T_i] must be a <>. The canonical type of the value is _{_ stem:[m_1] _:_ stem:[T_1] _,_ stem:[...] _,_ stem:[m_n] _:_ stem:[T_n] _}_. === Struct Values A *struct value* is a value associated with a <>. We write a struct value similarly to an <>, except that we annotate the value with a struct type: a struct value has the form `{` stem:[m_1] `:` stem:[v_1] `,` stem:[...] `,` stem:[m_n] `:` stem:[v_n] `}` `:` stem:[Q], where . stem:[Q] is a <> that refers to a <>. . The members of stem:[Q] are stem:[m_i] `:` stem:[T_i] for stem:[i in [1,n\]]. . For each stem:[i in [1,n]], stem:[v_i] is a value of type stem:[T_i]. Note that stem:[T_i] need not be a canonical type. For example, it is permissible for stem:[T_1] to be `T`, for `T` to be an alias of `U32`, and for stem:[v_1] to be the value `1: U32`. In this case `1: U32` is a value of type `T`, as required. Each member of the struct value must have an explicit value. The canonical type of the struct value is stem:[Q]. === Serialized Sizes Every value _v_ of a <> has a *serialized size*. This is the number of bytes required to represent _v_ in the standard F Prime serialized format. The serialized size _s_ of a value _v_ depends on the type _T_ of _v_: * If _T_ is a <>, then _s_ is the sum of the following two numbers: ** The serialized size of the <> `FwSizeStoreType`. This is the space used to store the length of the string. ** The length of the string in characters. * Otherwise if _v_ is an <>, then _s_ is the sum of the serialized sizes of the elements of _v_. * Otherwise if _v_ is a <>, then _s_ is the sum of the serialized sizes of the members of _v_ * Otherwise _s_ is the <>.