Change search
ReferencesLink to record
Permanent link

Direct link
Implementing a transational semantics for an imperative language
Number of Authors: 1
1990 (English)Report (Refereed)
Abstract [en]

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
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-21434OAI: diva2:1041470
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.Available from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(4373 kB)3 downloads
File information
File name FULLTEXT01.pdfFile size 4373 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 3 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 4 hits
ReferencesLink to record
Permanent link

Direct link