# Static Analysis for ECMAScript String Manipulation Programs
## 5 Abstract Semantics of ECMAScript String Operations
### Abstract Semantics of \(\mathsf{StartsWith}\)
```
Input : A = \((Q,\Sigma,\delta,q_{0},F)\), \(A^{\prime}=(Q^{\prime},\Sigma,\delta^{\prime},q^{\prime}_{0},F^{\prime})\) Output :SW\({}^{\sharp}(\texttt{A},\texttt{A}^{\prime})\)
1 if\(A^{\prime}==\text{Min}(\{\epsilon\})\)then
2 return\(\{\text{true}\}\);
3
4 end if
5 if\(\text{PR}(\texttt{A})\sqcap_{\text{\tiny{box}}}A^{\prime}==\text{Min}( \varnothing)\)then
6 return\(\{\text{false}\}\);
7
8 end if
9 if\(\text{hasCycle}(\texttt{A})\vee\text{hasCycle}(\texttt{A}^{\prime})\)then
10 return\(\top_{\text{Bool}}\);
11
12 end if
13 if\(\text{isSinglePath}(\texttt{A}^{\prime})\)then
14\(\texttt{B}\leftarrow\text{maxString}(\texttt{A}^{\prime})\);
15\(\texttt{C}\leftarrow\text{SS}^{\sharp}(\texttt{A},0,\texttt{LE}^{\sharp}( \texttt{B}))\);
16 if\(\texttt{B}==\texttt{C}\)then
17 return\(\{\text{true}\}\);
18
19 end if
20
21 end if return\(\top_{\text{Bool}}\);
```  
**Algorithm 2**SW\({}^{\sharp}:\text{DFA}_{/=}\times\text{DFA}_{/=}\rightarrow\mathbb{B}^{\sharp}\) algorithm  
In order to explain our approach in lines 10-17, consider the automata A and A\({}^{\prime}\) reported in Figure 9. To be sure that any string recognized by A\({}^{\prime}\) is the beginning of any string recognized by A we need to check two conditions: (1) any string recognized by A\({}^{\prime}\) is prefix of its longest recognized string \(\sigma\) and (2) each string in A starts with \(\sigma\) (all strings must have a common prefix). Only if both conditions occur we can safely return \(\{\text{true}\}\) otherwise we return \(\top_{\text{Bool}}\). In particular, (1) is checked by the function isSinglePath at line 10 and (2) is checked at lines 11-15. It is worth noting that if an automaton is single-path, then the longest string is unique (line 11). In our example, both the strings \(p\) and \(pan\) in \(\mathcal{L}(\texttt{A}^{\prime})\) are prefixes of \(pan\), which is the longest string recognized by A\({}^{\prime}\), so we build B, which is the (minimal) automaton that recognizes \(pan\) and \(\texttt{C}\), \(\mathcal{L}(\texttt{C})=\{pan,koa\}\), and compare them (line 13). We return \(\{\text{true}\}\) if B and C recognize the same language otherwise we return \(\top_{\text{Bool}}\). In the other cases, as already mentioned, we return \(\{\text{true},\text{false}\}\). For example, in Figure 9, \(\{\text{true},\text{false}\}\) is returned because, although A\({}^{\prime}\) is a single-path automaton, only the string \(panda\in\mathcal{L}(\texttt{A})\) begins with \(pan\), namely the longest string of \(\mathcal{L}(\texttt{A}^{\prime})\). **Example 2**. : _Consider for example A.s.t. \(\mathcal{L}(\texttt{A})=\{panda,panem\}\), and A\({}^{\prime}\)s.t. \(\mathcal{L}(\texttt{A}^{\prime})=\{p,pan\}\). \(\text{SW}^{\sharp}(\texttt{A},\texttt{A}^{\prime})\) returns \(\{\text{true}\}\) since A\({}^{\prime}\) is a single-path automaton and both strings of A start with the longest string in A\({}^{\prime}\), the string \(pan\). Consider instead the automata A, \(\mathcal{L}(\texttt{A})=\{panda,koa\}\), and A\({}^{\prime}\)s.t. \(\mathcal{L}(\texttt{A})=\{p,k\}\). In this case, \(\text{SW}^{\sharp}(\texttt{A},\texttt{A}^{\prime})\) returns \(\{\text{true},\text{false}\}\) since A\({}^{\prime}\) is not a single-path automaton. Indeed, we can easily check that even if the string \(panda\in\mathcal{L}(\texttt{A})\) starts with \(p\in\mathcal{L}(\texttt{A}^{\prime})\), the string \(koa\in\mathcal{L}(\texttt{A})\) does not._  
**Theorem 6**. : \(\text{SW}^{\sharp}\) _is sound but not complete. Formally,_  
\[\forall\texttt{A},\texttt{A}^{\prime}\in\text{DFA}_{/=}.\text{SW}(\mathcal{L}( \texttt{A}),\mathcal{L}(\texttt{A}^{\prime}))\subseteq\text{SW}^{\sharp}( \texttt{A},\texttt{A}^{\prime})\]As a counterexample to completeness, consider the automata A s.t. \(\mathcal{L}(\texttt{A})=\texttt{A}=\{\;a^{n}\;|\;n>1\;\}\) and \(\texttt{A}^{\prime}\) s.t. \(\mathcal{L}(\texttt{A}^{\prime})=\{a\}\).