Sciweavers

Share
FAC
2010

Blaming the client: on data refinement in the presence of pointers

9 years 5 months ago
Blaming the client: on data refinement in the presence of pointers
Data refinement is a common approach to reasoning about programs, based on establishing that te program indeed satisfies all the required properties imposed by an intended abstract pattern. Reasoning about programs in this setting becomes complex when use of pointers is assumed and, moreover, a well-known method for proving data refinement, namely the forward simulation method, becomes unsound in presence of pointers. The reason for unsoundness is the failure of the "lifting theorem" for simulations: imulation between abstract and concrete modules can be lifted to all client programs. The result is ulation does not imply that a concrete can replace an abstract module in all contexts. Our diagnosis of this problem is that unsoundness is due to interference from the client programs. Rather than blame a module for the unsoundness of lifting simulations, our analysis places the blame on the client programs which cause the interference: when interference is not present, soundness ...
Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where FAC
Authors Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang
Comments (0)
books