Jolie Static Type Checker: a prototype
This work addresses software reliability for developers using the Jolie language by providing a static type checker, but it is incremental as it implements an existing formal definition.
The authors tackled the lack of a static type checker for the Jolie programming language, which currently relies on dynamic typing and allows avoidable run-time errors, by implementing a prototype called JSTC that uses an SMT solver for static analysis.
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 dynamic 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.