DENOTATIONAL SEMANTICS FOR occam 2

Abstract

This paper gives an untimed denotational semantics for the concurrent programming language occam 2. It draws heavily on the semantics for a large subset of proto-occam[26],but addresses the complete extended language (to the extend that the model allows). The semantic domain used is a ‘failures divergences’ model, modified to allow machine states to be properly dealt with. This means that issues of fairness and priority are not addressed.