References & Citations
Computer Science > Software Engineering
Title: Jolie Static Type Checker: a prototype
(Submitted on 23 Feb 2017 (v1), last revised 18 Oct 2017 (this version, v5))
Abstract: 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.
Submission history
From: Manuel Mazzara [view email][v1] Thu, 23 Feb 2017 09:38:11 GMT (45kb,D)
[v2] Sat, 16 Sep 2017 08:20:53 GMT (43kb,D)
[v3] Tue, 19 Sep 2017 07:51:20 GMT (0kb,I)
[v4] Wed, 20 Sep 2017 11:30:33 GMT (44kb,D)
[v5] Wed, 18 Oct 2017 15:53:47 GMT (45kb,D)
Link back to: arXiv, form interface, contact.