Preserving Progress Under Program Composition Notes on UNITY: 17-90
Jayadev Misra · 2004
Introduction The question considered in this note is this: Under what condition is a progress property of program F preserved when F is composed with another program? For safety properties and progress properties of the form p ensures q, the corresponding question is answered by the union theorem. For general progress properties, however, there seems to be no easy answer; plausible rules, such as the following, are all invalid. p 7! q in F ; p stable in G p 7! q in F [] G p 7! q in F ; p 7! q in G p 7! q in F [] G One restriction we can put on G is that it should not write into any variable that it shares with F . It is then true that p 7! q in<