# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 3 Methodology
### Applying the Verifier Model to a Translator Case Study  
In this paper, we applied the TC-Verifier on the Swift to Java translator [17] as a proof of concept for our methodology. However, our methodology can be applied to any transcompiler-based high-level-to-high-level code translator that follows the similar translation method, depending on parsing and defining translation rules. The code statement translation process is the behavior of the translator for each code statement in the Swift source language. A code statement, in our context, is a concrete code structure unit that has a grammar rule and can be broken down into other rules. For example, variable declaration, class declaration, and function declaration will be considered code statements. Each code statement translation process is modeled using states and transitions in Uppaal. The real translator iterates all the input code line by line in a loop. In each loop iteration, a code statement translation process is triggered. However, for simplifying, we will model each code statement translation separately. This will also allow us to have a more specific interpretation of the output of the verifier. In the following paragraphs, we will explain the modeling process for the variable declaration statement to explain our modeling methodology. The same method is applied to the rest of the statement types that we cover in our experiment. We modeled the transition between the translator functions by transitions between states. The code starts from the main function and once the visit-java-top-rule function is visited, it goes to the next state. We represented the function visited trigger by a Boolean variable \"visit-java-top\". From the visit-java-top-rule function according to the parser that the translator is following, it should visit the next function according to the type of the input statement to be translated. Figure 2 shows a model example for the variable declaration translation process. For the variable declaration state machine, we declared a Bool _variabled declaration_. The guard of transition checks the value of this Bool variable: if it is true, it will continue to the next state. According to the grammar of the input language, Swift in our case, the variable declaration rule has six different productions. We modeled the translator's behavior when each of the six possible declarations was encountered. The variable declaration rule is shown in Figure 3.  
Figure 2: The state machine for variable declaration translation behavior on the trans-compiler using the Uppaal model checker. We encoded the Swift identifier as a Boolean. If the swift identifier \(swift\)-\(id\) is found and read by the parser, it means that it is valid. The rule of the Java identifier is the same as the Swift identifier. Therefore, the Java identifier variable \(Java\)-\(id\) is assigned the Swift identifier value which is True for a valid identifier. The translator in reality obtains the swift variable datatype and maps it through its database to the equivalent data type in Java. However, to implement this in UPPAAL, we needed variable strings, not constant ones, to model this process. Therefore, we had to do some encoding. We mapped the main datatypes of the Swift language to an array of integers named \(swift\)-\(types\). The corresponding Java datatypes are mapped to integers too. A function \(map\)-\(data\)-\(type\) is implemented to map each Swift data type to its corresponding Java data type. The Swift type array has eight integers. The elements from 0 to 6 represent the main swift data types like Int, Float, Double, etc. The element Swift-type[7] represents any user-defined data type. After the map function is triggered from the node \(type\)-\(annotation\) to the node \(java\)-\(type\)-\(return\), a guard checks the value of the Javatype variable. The transition to the next state Java-variable-decl will not happen unless the Javatype is assigned a value, i.e., a value that represents one of the mapped Java types like int, float, double, etc.