Sciweavers

Share
TOPLAS
2002

Data abstraction and information hiding

8 years 3 months ago
Data abstraction and information hiding
traction and information hiding K. RUSTAN M. LEINO and GREG NELSON Compaq Systems Research Center er describes an approach for verifying programs in the presence of data abstraction and information hiding, which are key features of modern programming languages with objects and modules. The paper draws on our experience building and using an automatic program checker, and focuses on the property of modular soundness: that is, the property that the separate verifications of the individual modules of a program suffice to ensure the correctness of the composite program. We found this desirable property surprisingly difficult to achieve. A key feature of our ogy for modular soundness is a new specification construct: the abstraction dependency, veals which concrete variables appear in the representation of a given abstract variable, revealing the abstraction function itself. This paper discusses in detail two varieties of ion dependencies: static and dynamic. The paper also presents a new t...
K. Rustan M. Leino, Greg Nelson
Added 23 Dec 2010
Updated 23 Dec 2010
Type Journal
Year 2002
Where TOPLAS
Authors K. Rustan M. Leino, Greg Nelson
Comments (0)
books