Implementing a transational semantics for an imperative language
Number of Authors: 1
1990 (English)Report (Refereed)
We present a semantics for an imperative programming language, Lunsen, with constructs for concurrency and communication. The semantics is given through a translation into CCS. This translation has been implemented within the framework of the Concurrency Workbench, which is a tool for analysis of finite-state systems in CCS. The point of the translational semantics is that by imposing restrictions on Lunsen, so that the semantics of a program is finite-state, we can analyze Lunsen programs automatically using the Concurrency Workbench. We illustrate this by analyzing the alternating bit algorithm and two mutual exclusion algorithms.
Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1990, 4. , 45 p.
SICS Technical Report, ISSN 1100-3154 ; T90:05
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-14123OAI: oai:DiVA.org:ri-14123DiVA: diva2:1035407
This paper is an extended version of an earlier paper : " An Implementation of a Translational Semantics for an Imperative Language" by L.Fredlund, B. Jonsson and J. Parow. Published in Proceedings of CONCUR'90 conference on Theories of Concurrency, Unification and Extension. Springer-Verlag, Volume 458, 1990, Pages 246-262. Original report number T90005.2016-10-132016-10-13