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

Blaming the client: on data refinement in the presence of pointers,10.1007/s00165-009-0125-8,Formal Aspects of Computing,Ivana Filipovic,Peter W. O'He

Blaming the client: on data refinement in the presence of pointers   (Citations: 1)
BibTex | RIS | RefWorks Download
Data refinement is a common approach to reasoning about programs, based on establishing that a concrete 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: that a simulation between abstract and concrete modules can be lifted to all client programs. The result is that simulation 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 is recovered. Technically, we present a novel instrumented semantics which is capable of detecting interference between a module and its client. With use of special simulation relations, namely growing relations, and interpreting the simulation method using the instrumented semantics, we obtain a lifting theorem. We then show situations under which simulation does indeed imply refinement.
Journal: Formal Aspects of Computing - FAC , vol. 22, no. 5, pp. 547-583, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Filipovi´ c, O’Hearn, Torp-Smith, and Yang ([5]); Mijajlovi´ c et al. ([9]) previously considered data refinement for local reasoning, studying modules built on the heap model...
    • ...By contrast with Filipovi´ c et al. ([5]), we work with the axiomatic semantics, rather than operational semantics, of the language, defining proof transformations that establish that concrete implementations simulate abstract specifications...

    Thomas Dinsdale-Younget al. Abstract Local Reasoning for Program Modules

Sort by: