## 4 Concrete Domain and Semantics
### Concrete Semantics  
To formalize the concrete semantics of the \(\mathcal{C}\) standard library functions from string.h introduced in Section 3, the following auxiliary functions _embedding_, _extraction_, _comparison_ and _substitution_ over single concrete character array values need to be introduced. **Definition 2** (embedding). : _Let \(\mu(\mathfrak{m}_{1}),\mu(\mathfrak{m}_{2})\in\mathbf{M}\) be two concrete character array values and \([\mathfrak{l}_{1},\mathfrak{u}_{1}]\subseteq[[\! [\mathrm{low}_{\mathfrak{m}_{1 }}]\!]\!]\! ]\!,[\mathfrak{h}[  
**Function:**\(comparison(\mu(m_{1}),\mu(m_{2}))\)  
**Input:** two concrete character array values \(\mu(m_{1})\), \(\mu(m_{2})\in\mathbf{M}\) such that:  
* both \(N_{m_{1}}\) and \(N_{m_{2}}\) are different from the emptyset and,
* for \(i_{1}\in[\![\![\mathrm{low}_{m_{1}}]\!]\!]\!,min(N_{m_{1}})),i_{2}\in[\![\! [ \mathrm{low}_{m_{2}}]\! ]\!,min(N_{m_{2}}))\): \(M(i_{1})\
eq(i_{1},\top_{C})\) and \(M(i_{2})\
eq(i_{2},\top_{C})\)  
**Output:** an integer value \(n\). ```
1:n = 0, \(i_{1}=[\![\mathrm{low}_{m_{1}}]\!]\!]\!,i_{2}=[\![\mathrm{low}_{m_{2}}]\! ]\!\rho\)
2:while\(i_{1}\in[\![\mathrm{low}_{m_{1}}]\!]\! ]\!,min(N_{m_{1}})\)] and \(i_{2}\in[\![\![\mathrm{low}_{m_{2}}]\!]\! ]\!,min(N_{m_{2}})]\)do
3:n = \(v_{i_{1}}\)\({}_{\frown}\)\(v_{i_{2}}\)
4:ifn \(\
eq 0\)then
5:return n
6:else
7:\(i_{1}=i_{1}+1\)
8:\(i_{2}=i_{2}+1\)
9:return n
```  
**Algorithm 1** Lexicographic comparison of concrete character array values. **Definition 3** (extraction). : _Let \(\mu(m)\in\mathbf{M}\) be a concrete character array value and \([\![\mathrm{l},u]\!]\subseteq[\![\mathrm{low}_{m}]\!]\!,[\![\mathrm{high}_{m}]\!]\! ]\!\rho\) be an indexes range. The function \(extraction(\mu(m),[\![\mathrm{l},u]\! ])\) extracts the sequence of characters which occurs in \(\mu(m)\) from the index \(1\) to the index \(u\). Formally, \(extraction(\mu(m),[\![\mathrm{l},u]\! ])=\mu(m)^{\prime}\) such that:_  
* \([\![\mathrm{low}_{m^{\prime}}]\!]\!]\! ]\!=\!1\) _and_ \([\![\mathrm{high}_{m^{\prime}}]\!]\!]\! ]\!=\!u+1\)__
* \(\mathcal{M}_{m^{\prime}}:\forall i\in[\![\mathrm{low}_{m^{\prime}}]\!]\!]\! [ \rho,[\mathrm{high}_{m^{\prime}}]\!]\!]\! :\mathcal{M}_{m^{\prime}}(i)=(i,v)\)_s.t._ \(k=i\) _and_ \(\mathcal{M}_{m}(k)=(k,v)\)__
* \(N_{m^{\prime}}=N_{m}\setminus\{i\ |\ i\
ot\in[\![\mathrm{l},u]\! ]\!\}\)__  
**Example 7**. : _Let \(\mu(m_{1})\) be the character array concrete value of Example 6 and \([\![1,3]\!]_{m_{1}}\subseteq[\![\mathrm{low}_{m_{1}}]\!]\!,[\! [\mathrm{high}_{m _{1}}]\!]\! ]\!\rho\), \([\![\mathrm{high}_{m_{1}}]\!]\! ]\!\rho\) be an indexes range of \(\mu(m_{1})\). The function \(extraction(\mu(m_{1}),[\![1,3]\! ]_{m_{1}})=\mu(m_{1})^{\prime}\) such that:_  
* \([\![\mathrm{low}_{m^{\prime}_{1}}]\!]\!]\! ]\!=\!1\) _and_ \([\![\mathrm{high}_{m^{\prime}_{1}}]\!]\!]\! ]\!=\!4\)__
* \(P_{m^{\prime}_{1}}=\{(1,\text{'a'}),(2,\text{'a'}),(3,\text{'0'})\}\)__
* \(N_{m^{\prime}_{1}}=\{3\}\)__  
**Definition 4** (comparison). : _Let \(\mu(m_{1})\), \(\mu(m_{2})\in\mathbf{M}\) be two concrete character array values which contain a fully initialized well-formed string of interest, i.e., no \(\top_{C}\) occurs. The function \(comparison(\mu(m_{1}),\mu(m_{2}))\) (c.f. Algorithm 1) lexicographically compares the strings of interest of \(\mu(m_{1})\) and \(\mu(m_{2})\) and it returns an integer value \(n\) which denotes the lexicographic distance between them._  
_Notice that \(n\) will be strictly smaller than zero if \(string(\mu(m_{1}))\) precedes string\((\mu(m_{2}))\) in lexicographic order, equal to zero if \(string(\mu(m_{1}))\) and \(string(\mu(m_{2}))\) are lexicographically equivalent, and strictly greater than zero if \(string(\mu(m_{1}))\) follows \(string(\mu(m_{2}))\) in lexicographic order._  
**Example 8**. : _Let \(\mu(m_{1})\) and \(\mu(m_{2})\) be the character array concrete values of Example 6. Both of them contain a fully initialized well-formed string of interest and the function \(comparison(\mu(m_{1}),\mu(m_{2}))\) computes the lexicographic distance between them.