Department of Computer Science and Technology

Technical reports

On the composition and decomposition of assertions

Glynn Winskel

November 1984, 35 pages

Abstract

Recently there has been a great deal of interest in the problem of how to compose modal assertions, in order to deduce the truth of an assertion for a composition of processes in a parallel programming language, from the truth of certain assertions for its components.

This paper addresses that problem from a theoretical standpoint. The programming language used is Robin Milner’s Synchronous Calculus of Communicating Systems (called SCCS), while the language of assertions is a fragment of dynamic logic which, despite its simplicity, is expressive enough to characterise observational equivalence. It is shown how, with respect to each operation ‘op’ in SCCS, every assertion has a decomposition which reduces the problem of proving the assertion holds of a compound process built up using ‘op’ to proving assertions about its components. These results provide the foundations of a proof system for SCCS with assertions.

Full text

PDF (1.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-59,
  author =	 {Winskel, Glynn},
  title = 	 {{On the composition and decomposition of assertions}},
  year = 	 1984,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-59.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-59}
}