The role of auxiliary variables in the formal development of concurrent programs (2009)

Author(s): Jones CB

    Abstract: 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.

      • Date: November 2009
      • Series Title: School of Computing Science Technical Report Series
      • Institution: School of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

      Keywords: Concurrency, Rely/Guarantee, formal methods

      Staff

      Professor Cliff Jones
      Professor
      • Telephone: +44 191 222 8183