# Static Analysis for ECMAScript String Manipulation Programs
## 3 The Core Language
### Semantics  
In \(\mu\)JS the primitive values are \(\mathbb{V}=\mathbb{S}\cup\mathbb{Z}\cup\mathbb{B}\cup\{\mathtt{NaN}\}\) with \(\mathbb{S}\stackrel{{\text{\tiny{\raisebox{0.0 pt}[0.0 pt][0.0 pt]{ \tiny{\raisebox{0.0 pt}[0. \(\texttt{Exp}\times\texttt{States}\rightarrow\mathbb{V}\), is standard and follows [18]; we only provide the formal and precise semantics of the \(\mu\)JS string operations. Let \(\sigma,\sigma^{\prime}\in\mathbb{S}\) and \(i,j\in\mathbb{Z}\) (values which are not strings or numbers respectively, are converted by the implicit type conversion primitives, moreover, negative values are treated as zero). **substring:**: It extracts the substring between two indexes from a string. The semantics is defined by the function \(\texttt{Ss}\colon\mathbb{S}\times\mathbb{Z}\times\mathbb{Z}\rightarrow\mathbb{S}\) as:  
\[\texttt{Ss}(\sigma,i,j)\stackrel{{\text{\tiny def}}}{{=}} \begin{cases} \texttt{Ss}(\sigma,j,i)&j<i\\ \sigma_{i}\ldots\sigma_{j}&j<|\sigma|\ \wedge\ i\leq\ j\\ \sigma_{i}\ldots\sigma_{n}&j\geq n=|\sigma|\wedge\ i\leq j\end{cases} \]
**charAt:**: It returns the character, i.e., the string of unitary length, at a specified index in a string \(\sigma\). The semantics is the function \(\texttt{Ca}\colon\mathbb{S}\times\mathbb{Z}\rightarrow\mathbb{S}\) defined as follows:  
\[\texttt{Ca}(\sigma,i)\stackrel{{\text{\tiny def}}}{{=}} \begin{cases} \sigma_{i}&0\leq i<|\sigma|\\ \epsilon&\text{otherwise}\end{cases} \]
**length:**: It returns the length of a string \(\sigma\in\mathbb{S}\). Its semantics is the function \(\texttt{Le}\colon\mathbb{S}\rightarrow\mathbb{Z}\) defined as \(\texttt{Le}(\sigma)\stackrel{{\text{\tiny def}}}{{=}}|\sigma|\). **concat:**: It returns the concatenation between two strings and its concrete semantics \(\texttt{Cc}\colon\mathbb{S}\times\mathbb{S}\rightarrow\mathbb{S}\) relies on the concatenation operator reported in Section 2. \[\texttt{Cc}(\sigma,\sigma^{\prime})=\sigma\cdot\sigma^{\prime}\]
**startsWith:**: It determines whether a specified string \(\sigma\) starts with \(\sigma^{\prime}\). The semantics is the function \(\texttt{Sw}\colon\mathbb{S}\times\mathbb{S}\rightarrow\mathbb{B}\) defined as:  
\[\texttt{Sw}(\sigma,\sigma^{\prime})\stackrel{{\text{\tiny def}}}{{=}} \begin{cases}\texttt{true}&\exists\sigma^{\prime\prime}\in\Sigma^{*}.\sigma= \sigma^{\prime}\cdot\sigma^{\prime\prime}\\ \texttt{false}&\text{otherwise}\end{cases} \]
**repeat:**: It returns the given string repeated \(n\) times. The semantics is the function \(\texttt{Rt}\colon\mathbb{S}\times\mathbb{Z}\rightarrow\mathbb{S}\) defined as \(\texttt{Rt}(\sigma,n)\stackrel{{\text{\tiny def}}}{{=}}\sigma^{n}\). **includes:**: It determines whether a string \(\sigma^{\prime}\) is a substring of \(\sigma\). The semantics is the function \(\mathbb{N}\times\mathbb{S}\rightarrow\mathbb{B}\) defined as:  
\[\texttt{In}(\sigma,\sigma^{\prime})\stackrel{{\text{\tiny def}}}{{=}} \begin{cases}\texttt{true}&\exists\phi,\psi\in\Sigma^{*}.\sigma=\phi\cdot\sigma^ {\prime}\cdot\psi\\ \texttt{false}&\text{otherwise}\end{cases} \]
**toLowerCase:**: It returns the given string in all lowercase letters. The semantics is the function \(\texttt{Lc}\)\(\texttt{:}\mathbb{S}\rightarrow\mathbb{S}\) defined as \(\texttt{Lc}(\sigma)\stackrel{{\text{\tiny def}}}{{=}}\texttt{to LowerCase}(\sigma)\). **trimLeft:**: It removes all the white-spaces at the beginning of a string. The semantics is the function \(\texttt{TL}\colon\mathbb{S}\rightarrow\mathbb{S}\) defined as:  
\[\texttt{TL}(\sigma)\stackrel{{\text{\tiny def}}}{{=}}\sigma^{ \prime}\quad\text{where }\psi=\texttt{max}\{\;\psi^{\prime}\in(\_)^{*}\mid\sigma=\psi^{\prime}\cdot \sigma^{\prime}\;\}\wedge\sigma=\psi\cdot\sigma^{\prime}\]
**trimRight:**: It removes all the white-spaces at the end of a string.