A Denotational Semantics for Communicating Unstructured Code

Nils Jähnig
(TU Berlin)
Thomas Göthel
(TU Berlin)
Sabine Glesner
(TU Berlin)

An important property of programming language semantics is that they should be compositional. However, unstructured low-level code contains goto-like commands making it hard to define a semantics that is compositional. In this paper, we follow the ideas of Saabas and Uustalu to structure low-level code. This gives us the possibility to define a compositional denotational semantics based on least fixed points to allow for the use of inductive verification methods. We capture the semantics of communication using finite traces similar to the denotations of CSP. In addition, we examine properties of this semantics and give an example that demonstrates reasoning about communication and jumps. With this semantics, we lay the foundations for a proof calculus that captures both, the semantics of unstructured low-level code and communication.

In Bara Buhnova, Lucia Happe and Jan Kofroň: Proceedings 12th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2015), London, United Kingdom, April 12th, 2015, Electronic Proceedings in Theoretical Computer Science 178, pp. 9–21.
Published: 17th March 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.178.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org