| | | A.2.8 Array Values, Updates, and Selections |
ARRAY(I:T): E
E WITH [E1]:=E2
E[E1]
The array value expression ARRAY(I:T): E denotes the array where every index I of type T is mapped to the element denoted by the expression E (in which I may freely occur). Correspondingly the type of the expression is the array type ARRAY T OF TE where TE is the type of E.
The array update expression E WITH [E1]:=E2 is composed of a value E of type ARRAY T1 OF T2 for some types T1 and T2, a value E1 of type T1 and a value E2 of type T2. It denotes the array that is identical to E except that index E1 is mapped to element E2. Correspondingly the type of the expression is also ARRAY T1 OF T2.
The array selection expression E[E1] is composed of a value E of type ARRAY T1 OF T2, for some types T1 and T2, and a value E1 of type T1. It denotes the element of E at index E1; correspondingly its type is T2.
| | | A.2.8 Array Values, Updates, and Selections |