Technical reports

Sequential program composition in UNITY

Tanja Vos, Doaitse Swierstra

March 2000, 20 pages

DOI: 10.48456/tr-487

Abstract

Large distributed applications are composed of basic blocks by using composition operators. In an ideal situation, one should be able to develop and verify each of these basic components by itself using compositionality theorems of the respective composition operators stating that properties of a composite program can be proved by proving properties of its components.

Generally two forms of distributed program composition can be distinguished: parallel composition and sequential composition. Parallel composition is standard in UNITY and is used when two distributed component-programs need to cooperate in one way or another. Sequential composition of UNITY programs is not part of core UNITY. It can however be very useful when we want a program to work with the results of another program. In this technical report we shall formally define and model sequential program composition within the HOL-UNITY embedding.

Full text

PDF (1.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-487,
  author =	 {Vos, Tanja and Swierstra, Doaitse},
  title = 	 {{Sequential program composition in UNITY}},
  year = 	 2000,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-487.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-487},
  number = 	 {UCAM-CL-TR-487}
}