Role of Auxiliary Variables in the Formal Development of Concurrent Programs

摘要

So called auxiliary variables are often used in reasoning about concurrent programs. They can be useful--but they can also be undesirable in that they can undermine the hard won property of compositionality. This paper explores the issue of auxiliary variables and tries to set concerns about overuse in a wider context; it concludes with an attempt to recommend constraints on their use.