zbMATH — the first resource for mathematics

Denotational semantics of a parallel object-oriented language. (English) Zbl 0695.68058
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.
Reviewer: G.Saake

68Q55 Semantics in the theory of computing
68N99 Theory of software
68N25 Theory of operating systems
Ada95; Smalltalk; POOL
Full Text: DOI
[1] America, P., Definition of the programming language POOL-T, (), No. 0091
[2] America, P., Rationale for the design of POOL, (), No. 0053
[3] America, P., POOL-T—A parallel object-oriented language, ()
[4] America, P.; De Bakker, J.W., Designing equivalent semantic models for process creation, Theoret. comput. sci., 60, 109-176, (1988) · Zbl 0652.68029
[5] America, P.; De Bakker, J.W.; Kok, J.N.; Rutten, J.J.M.M., Operational semantics of a parallel object-oriented language, (), 194-208
[6] America, P.; Rutten, J.J.M.M., Solving reflexive domain equations in a category of complete metric spaces, (), 254-288
[7] To appear in J. Comput. System Sci.
[8] ANSI, (), ANSI/MIL-STD 1815 A
[9] Bergstra, J.; Klop, J.W., Process algebra for synchronous communication, Inform. and control, 60, 109-137, (1984) · Zbl 0597.68027
[10] De Bakker, J.W.; Kok, J.N.; Meyer, J.-J.Ch.; Olderog, E.-R.; Zucker, J.I., Contrasting themes in the semantics of imperative concurrency, (), 51-121 · Zbl 0606.68019
[11] De Bakker, J.W.; Zucker, J.I., Processes and the denotational semantics of concurrency, Inform and control, 54, 70-120, (1982) · Zbl 0508.68011
[12] De Bruin, A., Experiments with continuation semantics: jumps, backtracking, dynamic networks, ()
[13] Clinger, W.D., Foundations of actor semantics, (), AI-TR-633
[14] Dugundji, J., Topology, (1966), Allyn & Bacon, Inc Boston · Zbl 0144.21501
[15] Engelking, R., ()
[16] Gierz, G.; Hofmann, K.H.; Keimel, K.; Lawson, J.D.; Mislove, M.; Scott, D.S., ()
[17] Goldberg, A.; Robson, D., ()
[18] Gordon, M.J.C., ()
[19] Hahn, H., ()
[20] Hennessy, M.; Plotkin, G.D., Full abstraction for a simple parallel programming language, (), 108-120 · Zbl 0457.68006
[21] Hewitt, C., Viewing control structures as patterns of passing messages, Artif. intell., 8, 323-364, (1977)
[22] Mac Lane, S., ()
[23] Odijk, E.A.M., The DOOM system and its applications: A survey of ESPRIT 415 subproject A, (), 461-479
[24] Rutten, J.J.M.M., Semantic correctness for a parallel object-oriented language, report CS-R8843, (), To appear in · Zbl 0697.68077
[25] Vaandrager, F.W., Process algebra semantics of POOL, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.