Jolie Static Type Checker: a Prototype
Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such app...
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2017-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/608 |
| _version_ | 1826559059085492224 |
|---|---|
| author | Daniel de Carvalho Manuel Mazzara Bogdan Mingela Larisa Safina Alexander Tchitchigin Nikolay Troshkov |
| author_facet | Daniel de Carvalho Manuel Mazzara Bogdan Mingela Larisa Safina Alexander Tchitchigin Nikolay Troshkov |
| author_sort | Daniel de Carvalho |
| collection | DOAJ |
| description | Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and the dynamic one checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis. The article is published in the authors’ wording. |
| first_indexed | 2024-04-10T02:26:33Z |
| format | Article |
| id | doaj.art-e7af9382c85f438691aeb4997468f4c9 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2025-03-14T08:54:22Z |
| publishDate | 2017-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-e7af9382c85f438691aeb4997468f4c92025-03-02T12:46:51ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172017-12-0124670471710.18255/1818-1015-2017-6-704-717442Jolie Static Type Checker: a PrototypeDaniel de Carvalho0Manuel Mazzara1Bogdan Mingela2Larisa Safina3Alexander Tchitchigin4Nikolay Troshkov5Innopolis UniversityInnopolis UniversityInnopolis UniversityInnopolis UniversityTypeable.io LLCInnopolis UniversityStatic verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and the dynamic one checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis. The article is published in the authors’ wording.https://www.mais-journal.ru/jour/article/view/608microservicestatic analysisjolie programming language |
| spellingShingle | Daniel de Carvalho Manuel Mazzara Bogdan Mingela Larisa Safina Alexander Tchitchigin Nikolay Troshkov Jolie Static Type Checker: a Prototype Моделирование и анализ информационных систем microservice static analysis jolie programming language |
| title | Jolie Static Type Checker: a Prototype |
| title_full | Jolie Static Type Checker: a Prototype |
| title_fullStr | Jolie Static Type Checker: a Prototype |
| title_full_unstemmed | Jolie Static Type Checker: a Prototype |
| title_short | Jolie Static Type Checker: a Prototype |
| title_sort | jolie static type checker a prototype |
| topic | microservice static analysis jolie programming language |
| url | https://www.mais-journal.ru/jour/article/view/608 |
| work_keys_str_mv | AT danieldecarvalho joliestatictypecheckeraprototype AT manuelmazzara joliestatictypecheckeraprototype AT bogdanmingela joliestatictypecheckeraprototype AT larisasafina joliestatictypecheckeraprototype AT alexandertchitchigin joliestatictypecheckeraprototype AT nikolaytroshkov joliestatictypecheckeraprototype |