A Calculus of Gamma Programs

The Gamma model is a minimal programming language based on local multiset rewriting (with an elegant chemical reaction metaphor); Hankin et al derived a calculus of Gamma programs built from basic reactions and two composition operators, and applied it to the study of relationships between parallel and sequential program composition, and related program transformations. The main shortcoming of the "calculus of Gamma programs" is that the refinement and equivalence laws described are not compositional, so that a refinement of a sub-program does not necessarily imply a refinement of the program. In this paper we address this problem by defining a compositional (denotational) semantics for Gamma, based on the transition trace method of Brookes, and by showing how this can be used to verify substitutive refinement laws, potentially widening the applicability and scalability of program transformations previously described. The compositional semantics is also useful in the study o...

• Type: Conference
• Year: 1992
• Where: LCPC
• Authors: Chris Hankin, Daniel Le Métayer, David Sands
• Keywords: Gamma, Gamma Model, Gamma Programs, LCPC 1992, System Software