Modular typestate checking of aliased objects

9 years 9 months ago
Modular typestate checking of aliased objects
Objects often define usage protocols that clients must follow in order for these objects to work properly. Aliasing makes it notoriously difficult to check whether clients and implementations are compliant with such protocols. Accordingly, existing approaches either operate globally or severely restrict aliasing. We have developed a sound modular protocol checking approach, based on typestates, that allows a great deal of flexibility in aliasing while guaranteeing the absence of protocol violations at runtime. The main technical contribution el abstraction, access permissions, that combines typestate and object aliasing information. In our methodology, developers express their protocol design intent through annotations based on access permissions. Our checking approach then tracks permissions through method implementations. For each object reference the checker keeps track of the degree of possible aliasing and is appropriately conservative in reasoning about that reference. This h...
Kevin Bierhoff, Jonathan Aldrich
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Authors Kevin Bierhoff, Jonathan Aldrich
Comments (0)