Denotational semantics of a parallel object-oriented language (Q910250)

The paper presents a formal semantics for the parallel object-oriented programming language POOL. POOL describes a system as a collection of communicating objects which are executed in parallel. The formal semantics of POOL programs is defined using a denotational framework based on a category of complete metric spaces. The semantics of language constructs is defined in a compositional way including such critical points like object creation and method invocation using messages. The semantics of an entire program is represented by a process allowing to deal with fairness properties. The introduction gives an overview of the basic concepts of the POOL language. The basic ideas of the denotational semantics definition are sketched and related to other approaches. The second section presents the basic definitions and properties of the formal framework used for the denotational semantics. After introducing the basic concepts of complete metric spaces, solutions of reflexive domain equations in complete metric spaces are discussed. The category of complete metric spaces is defined building the base for the denotational semantics. The language POOL is described in the third section in detail. A pool program is a collection of objects being dynamic entities containing state information (stored in variables) and methods. Objects can be created dynamically and interact by sending messages. An object collection is regarded as a collection of communicating parallel processes. Section 4 is the main part of the paper presenting the denotational semantics of POOL programs in a compositional way. The semantic construction is based on a domain P of processes. The semantics of POOL expressions and statements is defined using environments, objects, and continuations. The environment contains the meanings of classes and methods, whereas the object domain stands for the set of object names (which may change due to object creations). The continuation given as an argument of semantic functions describes what will happen after the execution of the current expression or statement. Standard processes model the basic objects of type integer and Boolean. The semantics of a POOL unit (a collection of object class definitions) is given by a process resulting from a fixed point construction starting with creation of one initial object. The fifth section discusses the notion of fairness as a property of objects and composed processes in the used semantical framework. An object evolution (called path) is characterized as unfair if a desired action (a computation step or a communication) of this object is never executed although there are infinitely many moments this action is enabled. The paper ends with a conclusion section and an appendix presenting the central fixed point construction for the parallel composition operator. Defining the formal semantics of (parallel) object-oriented languages is an important task even if there are only a few successful attempts until now. The paper by America et al. presents a global semantics for description of collections of independent communicating objects. The chosen language offers powerful constructs like dynamic object creation and flexible object communication. The concept of object has no direct counterpart in the semantic domain used for the denotational semantics which may be an interesting task for future considerations. The presented approach is clearly a major step towards formal frameworks for (parallel) object-oriented programming language semantics.