# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 3 Methodology
### Experimental Setup-Statements Covered  
This paper is considered the first round of iterative rounds to verify a complete trans-compiler inspired by the work performed by [16] to verify a compiler iteratively. To reach a complete verified Trans-compiler, the modeling should include all code statement types defined in the grammar of the input language. The grammar of Swift language, the input language in our case study, has nine types of statements. Declarations is one of the nine statements and it has sixteen declarations types. In this round, out of the sixteen declarations, we focused on three declaration types. The loop statement is the type of statement following the declaration statement, and we will model one type of loop statement out of four types as an example of another type of statement. the following paragraphs include details of modeling these statements:  
(1) Variable declaration statement: we modeled the six different productions of the variable declaration grammar rule. The model included the built-in datatypes and their translation rules. The variable initialization was excluded in this phase as it will need modeling many other recursive statements like expressions with all their types; postfix, prefix, primary, Boolean..., etc. Each of these expressions is a code statement on its own and has several productions. Expressions will be included in the upcoming phases of the verifier and are not included in this paper. We modeled 14 different possible symbols for the variable declaration statement. The different symbols represent the different productions of the variable declaration grammar rule. In addition, some symbols represent the main built-in data types of the Swift language and a symbol that represents any other data type. For each symbol, there is a query that checks the validity of paths given this input symbol,  
Figure 3: The grammar rule of variable declaration from the Swift language grammar file. plus two general invariantly and possibly queries explained in the last subsection and shown in Table 2.  
(2) Function declaration: The function declaration grammar rule has one production. However, the production has three optional non-terminals, as shown in Figure 4. Each non-terminal has a deeply nested grammar and is further defined by several different productions. We modeled 31 different paths that the model function declaration with all optional terms in the production. The IBaction function, which is the button action function in Swift, in addition to the override, are possible productions of the attribute term in the grammar rule. The paths also included the generic parameter clause, the where clause, the throw, the retthrow, and all built-in data types as parameters and as return types. We considered one parameter only as the same process will happen for any length of the parameters list. The function body part is excluded since it can contain any statement that has not yet been covered by the verifier in this phase. A number of 33 queries are checked for the function declaration model. They include the two main invariantly and possibly queries mentioned before and the queries for the 31 paths. The function declaration queries are shown in Table 3.