Sequential program composition in UNITY

摘要

Large distributed applications are composed of basic blocks, by using composition operators. In anudideal situation, one should be able to develop and verify each of these basic components by itself,udusing compositionality theorems of the respective composition operators stating that propertiesudof a composite program can be proved by proving properties of its components.udGenerally, two forms of distributed program composition can be distinguished: parallel compositionudand sequential composition. Parallel composition is standard in UNITY [CM89], and isudused when two distributed component-programs need to cooperate in one way or another. Compositionalityudtheorems of parallel composition on general progress properties are extensively studiedudin [CM89, Sin89a, Pra95]. Sequential composition of UNITY programs is not part of core UNITYud[CM89]. It can however be very useful when we want a program to work with the results of anotherudprogram. For example, for the Propogation of Information with Feedback (PIF) protocol [Seg83]:udelect a leader ;let the leader be the starter of the PIF protocoludIn [Mis90b], a brief and intuitive characterisation of sequential composition is given. In thisudtechnical report, we shall formally define and model sequential program composition within theudHOL-UNITY embedding described in [Pra95, Vos00] In order to do so, we introduce a new typeudof UNITY programs called UNITY+ programs which consist of sequentially composed UNITYudprograms. The semantics of a UNITY+ programs is then defined in terms of a UNITY programudthat models the desired behaviour of the sequential composition. Finally, safety and progressudoperators are defined for these UNITY+ programs, and compositionality theorems are derived.udFor those readers not familiar with UNITY and its embedding in HOL, Appendix A containsuda brief overview of it. For those readers that are familiar with UNITY, we have compiled anudextensive index that should enable the reader to start reading this technical report, looking upuddesired definitions in a demand-driven way.