<XML><RECORDS><RECORD><REFERENCE_TYPE>7</REFERENCE_TYPE><REFNUM>5317</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Hankin,C.L.</AUTHOR></AUTHORS><YEAR>1997</YEAR><TITLE>Gamma and the Logic of Transition Traces</TITLE><PLACE_PUBLISHED>Advances in Theory and Formal Methods of Computing</PLACE_PUBLISHED><PUBLISHER>Imperial College Press</PUBLISHER><PAGES>-</PAGES><LABEL>Gay:1997:5317</LABEL><KEYWORDS><KEYWORD>program logic</KEYWORD></KEYWORDS<ABSTRACT>Gamma is a language of conditional multiset rewrites, which can be seen either as a parallel programming language or as a specification language for parallel algorithms. Taking the latter view, we are interested in program refinement and formal techniques for reasoning about it. In the present paper we apply Abramsky's framework of \emph{domain theory in logical form}, to systematically develop a program logic for Gamma from a denotational semantics. Our semantics is a domain-theoretic reformulation of the \emph{transition trace semantics}, which was defined for Gamma by Sands and based on earlier work by Brookes. We obtain a logic and proof system which is sound for our chosen notion of operational approximation or refinement and, as we show by means of an example, can be used to reason about program correctness. A further interesting point is that our techniques should apply not only to Gamma but to more general situations in which transition trace semantics can be used.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/tfm96.pdf</URL></RECORD></RECORDS></XML>