# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 4 Results and Discussion
### Comparison with BLEU Score  
To evaluate the TC-Verifier and illustrate the difference between formal verification via a model checker and translation evaluation by BLEU score, we consider an input Swift statement and we prompted GPT4 to generate multiple Java translations for this statement, as shown in Table 11. GPT4 generated five translations. We tested all of them. Four translations were compiled successfully. The translation that did not compile was removed. Another translation, although compiled successfully, was also omitted since it depended on manually adding the numbers to the array one by one, and this would require multiple code statements that would lead to a very low BLEU score and would also include other grammar rules than the array declaration. Therefore, to accurately evaluate the translation, we also omitted this candidate. Then, we added the trans-compiler translation as the last row in Table 11. The trans-compiler translation is very similar to the translation number one in Table 11, except that the \"final\" keyword is generated as an equivalent to the \"let\" keyword in Swift. Any of the GPT4 did not generate the \"final\" keyword suggested translations. However, the generated codes are not functionally wrong or non-equivalent to the input code. It would just be more precise to use \"final\" and evaluating GPT4 is not the scope of this paper. According to the model checking methodology, whenever the translator verifier decides a code statement as verified, it means that, for any example of this code statement, the translation will be correct. However, for BLEU, each translation is evaluated independently and the BLEU score depends on comparing the evaluated translation and the reference translation. For our case study translator, the TC-Verifier tool verified the array \begin{table}
\begin{tabular}{l l} \hline \hline
**Query Comment** & **Result** \\ \hline \hline \
\begin{tabular}{l} Checks that all paths will either reach the end state or not result in a \\ deadlock. \\ Checks whether one condition is passed and leads to the end. \\ Checks whether multiple conditions are passed and lead to the end. \\ Checks whether an expression condition, the end will be reached. \\ Checks whether an availability condition is passed, the end will be reached. \\ Checks whether a case condition is passed, the end will be reached. \\ Checks whether a binding condition is passed, the end will be reached. \\ Checks whether the translation of a code block leads to the end state. \\ \end{tabular} &
\begin{tabular}{l} NOT satisfied \\ Satisfied \\ NOT satisfied \\ Satisfied \\ NOT satisfied \\ NOT satisfied \\ NOT satisfied \\ NOT satisfied \\ Satisfied \\ \end{tabular} \\ \hline \hline \end{tabular}
\end{table} 
Table 10: The TC-Verifier results for while statement. \begin{table}
\begin{tabular}{l l} \hline \hline
**Language** & **Code** \\ \hline \begin{tabular}{l} Swift \\ Translation 1 \\ \end{tabular} & \
\begin{tabular}{l} let numbers: [Int] = [1, 2, 3, 4, 5] \\ int[] numbers = {1, 2, 3, 4, 5}; \\ List<Integer> numbers = new ArrayList<> (Arrays.asList(1, 2, 3, 4, 5)); \\ Installation 3 \\ Trans-compiler translation \\ \end{tabular} &
\begin{tabular}{l} int[] numbers = new int[][1, 2, 3, 4, 5]; \\ final int[] numbers = {1, 2, 3, 4, 5}; \\ \end{tabular} \\ \hline \hline \end{tabular}
\end{table} 
Table 11: Swift array declaration and Java translations. declaration shown in the example. However, the BLEU score will differ according to the reference translation as shown in Table 12. Each column shows the BLEU score for the translation provided by the Swift to Java trans-compiler with a different translation from the translations shown in Table 11.  
As shown in Table 12 the BLEU score evaluator will give 100% only if the trans-compiler translation was set as the reference. In Benchmark datasets for code-to-code translations, there might only exist one reference translation. A translator can generate a translation with a slightly different code structure but equivalent functionality.