Implementing a transational semantics for an imperative language

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.
ID Code:2184
Deposited By:Vicki Carleson
Deposited On:14 Jan 2009
Last Modified:04 Apr 2011 16:18

Repository Staff Only: item control page