Technical reports
On the composition and decomposition of assertions
November 1984, 35 pages
DOI: 10.48456/tr-59
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}, doi = {10.48456/tr-59}, number = {UCAM-CL-TR-59} }