A refinement calculus for tuple spaces

It is fairly accepted that the realization of complex systems must be accomplished step by step from the initial specification, through a sequence of intermediate phases, to the final program. These development steps, linking a preliminary version, or description, of the program to a more detailed one, are usually called refinement steps, while the intermediate stages of a refinement process are called levels of abstraction. A refinement calculus is a means to support this modus operandi in program development, allowing linking different levels of abstraction; it introduces a precise relation between intermediate descriptions, and the rules to check whether the relation is satisfied.