- Denotational semantics for thread algebra
- The Journal of Logic and Algebraic Programming
- Volume | Issue number
- 74 | 2
- Pages (from-to)
- Document type
- Faculty of Science (FNWI)
- Informatics Institute (IVI)
This paper gives a denotational semantics for thread algebra (TA), an algebraic framework for the description and analysis of recent programming languages such as C# and Java [J.A. Bergstra, C.A. Middelburg, Thread algebra for strategic interleaving, Formal Aspects of Computing, in press. Preliminary version: Computing Science Report PGR0404: Sectie Software Engineering, University of Amsterdam]. We illustrate the technique taken from the metric topology of de Bakker and Zucker [J.W. Bakker, J.I. Zucker, Processes and the denotational semantics of concurrency. Inform. and Control, 54 (1/2) (1982) 70-120] to turn the domains of TA into complete metric spaces. We show that the complete metric space consisting of projective sequences is an appropriate domain for TA. By using Banach’s fixed point theorem, we prove that the specification of a regular thread determines a unique solution. We also give a structural operational semantics for thread algebra and its relation to our denotational semantics. Finally, we present a particular interleaving strategy for TA that deals with abstraction in a natural way.
- go to publisher's site
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.