# Static Analysis for ECMAScript String Manipulation Programs
## 5 Abstract Semantics of ECMAScript String Operations
### Abstract Semantics of TrimLeft, TrimRight and Trim  
In this section, we will show the abstract semantics of trimLeft, trimRight and trim operations. The abstract semantics of trimLeft is defined by the function \(\texttt{TL}^{\sharp}:\texttt{Dfa}_{/\equiv}\rightarrow\texttt{Dfa}_{/\equiv}\). In particular, it takes as input an automaton A and returns an automaton accepting the same strings of A removing, at the beginning of each string, consecutive white spaces, if present. In the following, we denote a white-space as \(\_\). The function is computed by Algorithm 6. The idea of algorithm is to iteratively replace white-space transitions from the initial state with \(\epsilon\)-transition (lines 5-7), while leaving the other transitions unaltered (lines 7-9). At each iteration, the resulting automaton is minimized, and hence determinized (line 11). This operation is repeated until the initial state has no white-space transitions, checking the condition that white-space is not a prefix of the automaton (line 3). In Figure 14 is depicted an example of application of our algorithm.  
```
Input :A = \((Q,\Sigma,\delta,q_{0},F)\) Output :TL\({}^{\sharp}(\texttt{A})\) \(\delta^{\prime}\leftarrow\delta\); R \(\leftarrow\) A; while\(\texttt{PR}(\texttt{R})\cap_{\texttt{Dfa}}\text{Min}(\{\_\})\)do foreach\((q_{0},c,q)\in\delta\)do if\(c==\_\)then \(\delta^{\prime}\leftarrow\delta\cup(q_{0},\epsilon,q)\) else \(\delta^{\prime}\leftarrow\delta\cup(q_{0},c,q)\)  end if \(\texttt{R}\leftarrow(Q,\Sigma,\delta^{\prime},q_{0},F)\); \(\text{Min}(\texttt{R})\);  end if  end for return R;
```  
**Algorithm 6**\(\texttt{TL}^{\sharp}:\texttt{Dfa}_{/\equiv}\rightarrow\texttt{Dfa}_{/\equiv}\) algorithm  
**Theorem 10**.: \(\texttt{TL}^{\sharp}\) _is sound and complete. Formally, \(\forall\texttt{A}\in\texttt{Dfa}_{/\equiv}\),_  
\[\texttt{TL}(\mathcal{L}(\texttt{A}))=\mathcal{L}(\texttt{TL}^{\sharp}(\texttt{ A}))\]The abstract semantics of trimRight can be defined in function of the already defined function \(\mathsf{TL}^{\sharp}\). Indeed, the abstract semantics \(\mathsf{TR}^{\sharp}:\mathsf{DFA}_{/\equiv}\to\mathsf{DFA}_{/\equiv}\) reserves the input automaton, applies \(\mathsf{TL}^{\sharp}\) and finally reverses again the so obtained automaton. Formally,  
\[\mathsf{TR}^{\sharp}\stackrel{{\text{\tiny{def}}}}{{=}}\mathsf{ reverse}(\mathsf{TL}^{\sharp}(\mathsf{reverse}(\mathsf{A}))\]  
Similarly, the abstract semantics of trim applies both the abstract semantics of trimLeft and trimRight. Thus, the abstract semantics of trim is captured by the function \(\mathsf{TM}^{\sharp}:\mathsf{DFA}_{/\equiv}\to\mathsf{DFA}_{/\equiv}\) and it is defined as  
\[\mathsf{TM}^{\sharp}(\mathsf{A})\stackrel{{\text{\tiny{def}}}}{{= }}\mathsf{TR}^{\sharp}(\mathsf{TL}^{\sharp}(\mathsf{A}))\]  
Theorem 11: \(\mathsf{TR}^{\sharp}\) _and \(\mathsf{TM}^{\sharp}\) are sound and complete. Formally, \(\forall\mathsf{A}\in\mathsf{DFA}_{/\equiv}\)_  
\[\mathsf{TR}(\mathcal{L}(\mathsf{A}))=\mathcal{L}(\mathsf{TR}^{\sharp}( \mathsf{A}))\qquad\mathsf{TM}(\mathcal{L}(\mathsf{A}))=\mathcal{L}(\mathsf{ TM}^{\sharp}(\mathsf{A}))\]  
Proof: The proof of \(\mathsf{TR}^{\sharp}\) follows from the completeness of \(\mathsf{TL}^{\sharp}\) and reverse operations, while the proof of \(\mathsf{TM}^{\sharp}\) follows from the completeness of \(\mathsf{TL}^{\sharp}\) and \(\mathsf{TR}^{\sharp}\).