## 2 Prerequisites
### Fun Array
#### 2.2.1 Array Concrete Semantics  
Let \(R_{a}\) be the set of concrete array environments. A concrete array environment \(\theta\in R_{a}\) maps array variables \(a\in\mathbb{A}\) to their values \(\theta(a)\in\mathbf{A}\), such that:  
* \(\theta(a)=(\rho,low_{a},high_{a},A_{a})\) and,
* \(\theta(a)\in\mathbf{A}=R_{v}\times\mathbb{E}\times\mathbb{E}\times(\mathbb{Z} \rightarrow(\mathbb{Z}\times V))\) where  
1. \(R_{v}\) is the set of concrete variable environments. A concrete variable environment \(\rho\in R_{v}\) maps variables (of basic types) \(x\in\mathbb{X}\) to their values \(\rho(x)\in V\).
2. \(\mathbb{E}\) is the set of program expressions made up of constants, variables, mathematical unary and binary operators. In the following, for simplicity, expressions are evaluated to integers. \(low_{a},high_{a}\in\mathbb{E}\) are expressions whose value, given by \([low_{a}]\rho\) and \([high_{a}]\rho\), respectively represents the lower bound and the upper bound of an array \(a\), i.e., the lower and the upper bound of its indexes range. According to the denotational semantics approach, in [6] the value of an arithmetic expression \(e\) is denoted by \([e]\rho\), where: (1) the double square brackets notation denotes the semantic evaluation function and, (2) \(\rho\) is an environment mapping program variables (which also may appear in \(e\)) to their value. Typically, \([\![x]\!]\rho\) is equivalent to \(\rho(x)\), with \(x\in\mathbb{X}\), and \([\![n]\!]\rho\), where \(n\) is a constant, is equivalent to \(n\) itself. Thus, for example, if \(e\) is the expression \(x-1\), its semantics \([\![x-1]\!]\rho\) is defined as \([\![x]\!]\rho-[\![1]\!]\rho\), which corresponds to \(\rho(x)-1\). Notice that the value of an upper bound of an array concrete value corresponds to the index immediately after the one that points to the last memory block allocated to the array when it has been initialized. As usual, array indexes are \(0\)-based.
3. \(\mathbb{Z}\) is the set of integer numbers and \(V\) is the set of values. Let \(I_{a}\) be the set of indexes \(i\) of an array \(a\), i.e., \(I_{a}=\{i\ |\ \ i\in[[low_{a}]\rho,[high_{a}]\rho)\subseteq\mathbb{Z}\) and, let \(P_{a}\) be the set of pairs \((i,v)\) such that \(v\) is the value of the element indexed by \(i\) in an array \(a\), i.e., \(P_{a}=\{(i,v)\ |\ \ i\in I_{a}\wedge[\![a]\!]\rho=v\in V\}\subseteq \mathbb{Z}\times V\). Thus, \(A_{a}:I_{a}\to P_{a}\) is a function mapping the indexes of an array \(a\) to their corresponding pairs (index, indexed array value).  
**Example 1**.: _Let \(a\) be a \(C\) integer array initialized as follows: \(a[5]=\{5,7,9,11,13\}\). The concrete value of \(a\) is given by the tuple \(\theta(a)=(\rho,0,5,A_{a})\), where the value of the lower and the upper bound of \(a\) are clear from the context and the codomain of the function \(A_{a}\) is the set \(P_{a}=\{(0,5),(1,7),(2,9),(3,11),(4,13)\}\). Moreover, let denote the sub-array of a from position 2 to 3 included, its concrete value is given by \(\theta(b)=(\rho,2,4,A_{b})\) such that \(P_{b}=\{(2,9),(3,11)\}\)._  
Observe that this array representation allows reasoning about the correspondence between shape components of an array and actual values of the array elements.