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

• Type: Journal
• Year: 2010
• Where: FAC
• Authors: Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang
• Keywords: Client Programs, Computer Networks, Data Refinement, FAC 2010, Simulation