Typed Programming Languages for Communicating Object Systems

Anglo-Portuguese Joint Research Programme, Treaty of Windsor B29/02, 2002-2003, between

Programme

The general aim of the project is to develop programming language constructs which facilitate the development of more reliable software, particularly in the area of concurrent object-oriented systems. Specifically, we aim to develop type systems which support the specification and verification of complex interactions between agents in a concurrent system. Examples of such interactions are network communication protocols, client-server protocols, and the correct use of high-level data structures implemented by objects. This proposal stems from independent but closely related research carried out by the partners in recent years. We have a number of approaches to the programming language issues identified above, which use similar programming constructs but interpret the core primitives in slightly different ways. We feel that the time has come to combine our efforts, in order to understand the relationship between these approaches and work out how best to develop our type systems into programming support tools for real object-oriented programming languages.

Description of proposed work

Our first aim is to understand the relationship between the different strands of our previous research. In [1,3,4] a communication channel, along which messages can be transmitted, is viewed as the location of an object, and messages are interpreted as method invocations; in [2] there are no explicit objects but essentially the same language primitives are used to control communication on channels which represent network connections. The session types of [1,2] specify complex patterns of communication, and correct typing guarantees that all messages are understood immediately by their recipients; the non-uniform types of [3] describe selective availability of object services and correct typing guarantees that all messages are understood eventually. Once we have clarified these differences, we will be able to decide which combination of primitives and interpretations is the best basis for the design of a sophisticated type system for concurrent object-oriented programming. The TyCO language [4] implemented by the Portuguese partners will provide a basis for experiments in programming with different versions of the type system.

We then want to move from the experimental language TyCO to an established object-oriented language such as Java. The building blocks of Java are organised differently from those of [1-4]: the object access channels of [1,3,4] do not occur explicitly in quite the same way, and the network communication channels of [2] are masked by objects whose methods give access to messages of different kinds. However, it is clear that the notions of correctness guaranteed by our type systems still make sense in the context of Java, so our second task is to find the right mapping between the two settings.

Finally we will design, and perhaps begin to implement, a type-based program analysis tool for Java. Rather than implement a new compiler for an extension of Java with a new type system, our intention is that type declarations relating to communication behaviour will be added to Java programs either as specially formatted comments or in a form that can be easily removed by a pre-processor. A type-checker, which can be applied to a program before compilation, will then analyse the communication behaviour for errors of the kind addressed by [1-3]. An important design goal is to minimise the type annotations which the programmer must supply, by producing annotated versions of standard class libraries and making extensive use of type inference when analysing user programs.