A Type System for the Jolie Language |
Julie Meinicke Nielsen
|
| Abstract | The Jolie Language is a general-purpose service-oriented programming language. Service-oriented programming languages are designed for writing applications to services in. A service is an entity in a loosely coupled distributed system which is structured after the Service-Oriented Computing (SOC) paradigm. The focus of SOC is to separate software engineering from application programming and therefore are services autonomous entities which communicate by exchanging messages [MGZ, TCBM06].
In Jolie messages are structured as trees. A variable in Jolie is a path in a data tree and the type of a data tree is a tree itself. Jolie provides a language for describing the types that are allowed to be communicated in a network. Communications are type checked at run-time when a message is received, and such type checking is not formally defined. The aim of this thesis is to introduce static type checking to the theoretical foundation of the core fragment of Jolie.
The way of structuring types and handling variables in Jolie creates some challenges for introducing type checking to Jolie: The type language provided by Jolie allows a subtree of a tree type to be optional. Equality of types must
therefore be handled with that in mind. Variables are not declared wherefore the manipulation of the program state must be inferred. Besides the design of Jolie, SOC itself is also challenging: The ability to specify the type of messages a service wants to receive does not prevent that an ill-formed service send a message with a wrong type. It is therefore necessary to formalize run-time type checking of incoming messages.
The contribution of this thesis is the design of a static type checker for the core fragment of Jolie. The type checker rejects networks of services in which a message is sent or received, where the message has a wrong type according to sender and receivers type specifications. This is formally proved along with the property that a well-typed network can not reduce to an ill-typed network. Furthermore the dynamic type checking of incoming messages is described formally. |
| Type | Master's thesis [Academic thesis] |
| Year | 2013 |
| Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science / DTU Co |
| Address | Matematiktorvet, Building 303B, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk |
| Series | M.Sc.-2013-74 |
| Note | DTU supervisor: Nicola Dragoni, ndra@dtu.dk, DTU Compute |
| Electronic version(s) | [pdf] |
| Publication link | http://www.compute.dtu.dk/English.aspx |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |