Fredlund, Lars-Åke (1990) Implementing a transational semantics for an imperative language. [SICS Report]
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.
|Item Type:||SICS Report|
|Additional Information:||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.|
|Deposited By:||Vicki Carleson|
|Deposited On:||14 Jan 2009|
|Last Modified:||04 Apr 2011 16:18|
Repository Staff Only: item control page