Semantic Correctness for a Parallel Object-Oriented Language
Jan J. M. M. Rutten · SIAM Journal on Computing · 1990
Different semantic models are studied for a language called POOL: parallel object-oriented language. It is a simplified version of POOL-T, a language that is actually used to write programs for a parallel machine. The most important aspect of this language is that it describes a system as a collection of communicating objects that all have internal activities which are executed in parallel. For POOL, operational and denotational semantics have been developed previously. The former aims at the intuitive operational meaning of the language, whereas the main characteristic of the latter is compositionality. In this paper, the author relates both models, which are quite different, and proves the semantic correctness of the denotational semantics with respect to the operational semantics. These semantic investigations take place in the mathematical framework of complete metric spaces. For the operational semantics a simple space of functions from states to compact sets of streams (which are sequences of states) is used; for the denotational semantics, a domain of processes is used, which is the solution of a reflexive domain equation over a category of complete metric spaces. The main mathematical tool we use is Banach’s theorem, which states that contractions on complete metric spaces have unique fixed points. Both the operational and the denotational semantics are reformulated and are presented, as well as many operators on the semantic domains, as the fixed point of a suitably defined contraction. In this way, a formal equivalence between both models is established. For this purpose, an intermediate domain, which is first compared to the operational model by means of an abstraction operator, is introduced. This function takes processes, which are treelike structures, as arguments and yields sets of streams as results. Next, it is shown that both intermediate and the denotational model are fixed points of the same contraction, from which their equality follows. From both facts, the main result of this study follows: The operational meaning of a POOL program is equal to the denotational meaning to which the abstraction operator is applied. In this manner, the correctness of the denotational semantics with respect to the operational semantics is established.