Abstract:

This paper explores a compositional approach to program specification, development and proof. We apply a theory of composition to a problem in distributed computing with the goal of understanding the strengths and weaknesses of this compositional approach.
First, we describe the theory briefly. Then we give a specification of a desired system. Next, we propose a design of the desired system as a composition of components and prove its correctness. Finally, we show how the proof can be reused for a slightly different compositional structure by using the concept of observation.
Michel Charpentier <>
Last modified: Thu Feb 10 13:36:56 EST 2000