Conditional and Closure Properties

The union theorem, introduced in section 8.2.3, is the main tool for the study of asynchronous compositions of programs. The major virtue of this theorem is that it provides a simple rule for deducing the co-properties and transient predicates of a system from those of its component boxes. The major shortcoming is that it does not provide a simple rule for deducing the leads-to properties of a system from those of its components. The only way we can use a progress property of a component, p→ q in F, to deduce a similar property of the system is to either (1) apply the union theorem for progress (see section 8.2.6), which requires introduction of a well-founded order over the values of the shared variables, or (2) exhibit the proof of p→ q in F and show that the other components do not falsify the proof steps. The first strategy is cumbersome, and the second defeats the whole purpose of modular program construction.