More Web Proxy on the site http://driver.im/

article

Open access

Data abstraction and information hiding

Authors:

K. Rustan M. Leino,

Greg NelsonAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 24, Issue 5

Pages 491 - 553

https://doi.org/10.1145/570886.570888

Published: 01 September 2002 Publication History

Abstract

This article 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. This article 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 methodology for modular soundness is a new specification construct: the abstraction dependency, which reveals which concrete variables appear in the representation of a given abstract variable, without revealing the abstraction function itself. This article discusses in detail two varieties of abstraction dependencies: static and dynamic. The article also presents a new technical definition of modular soundness as a monotonicity property of verifiability with respect to scope and uses this technical definition to formally prove the modular soundness of a programming discipline for static dependencies.

References

[1]

Aho, A. V., Sethi, R., and Ullman, J. D. 1986. Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, Mass.

[2]

Almeida, P. S. 1997. Balloon types: Controlling sharing of state in data types. In ECOOP'97---Object-Oriented Programming: 11th European Conference, M. Akşit and S. Matsuoka, Eds. Lecture Notes in Computer Science, vol. 1241. Springer-Verlag, New York, pp. 32--59.

[3]

American National Standards Institute, Inc. 1983. ANSI/MIL-STD-1815A-1983, The Programming Language Ada Reference Manual. Lecture Notes in Computer Science, vol. 155. Springer-Verlag, Berlin, Germany.

[4]

Back, R. J. R. 1980. Correctness Preserving Program Refinements: Proof Theory and Applications. Mathematical Centre Tracts, vol. 131. Mathematical Centre, Amsterdam.

[5]

Boyland, J. 2001. Alias burying: Unique variables without destructive reads. Softw. Pract. Exper. 31, 6 (May), 533--553.

[6]

Detlefs, D. L., Leino, K. R. M., and Nelson, G. 1998a. Wrestling with rep exposure. Research Report 156, Digital Equipment Corporation Systems Research Center. July.

[7]

Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998b. Extended static checking. Research Report 159, Compaq Systems Research Center. Dec.

[8]

Ellis, M. A. and Stroustrup, B. 1990. The Annotated C++ Reference Manual. Addison-Wesley, Reading, Mass.

[9]

Ernst, G. W., Hookway, R. J., and Ogden, W. F. 1994. Modular verification of data abstractions with shared realizations. IEEE Trans. Softw. Eng. 20, 4 (Apr.), 288--307.

[10]

Extended Static Checking for Java. Extended Static Checking for Java home page. On the web at http://research.compaq.com/SRC/esc/.

[11]

Extended Static Checking for Modula-3. Extended Static Checking for Modula-3 home page. On the web at http://research.compaq.com/SRC/esc/EscModula3.html.

[12]

Gardiner, P. H. B. and Morgan, C. 1993. A single complete rule for data refinement. Form. Asp. Comput. 5, 4, 367--382.

[13]

Gosling, J., Joy, B., and Steele, G. 1996. The Javatm Language Specification. Addison-Wesley, Reading Mass.

[14]

Gries, D. and Prins, J. 1985. A new notion of encapsulation. In Proceedings of the ACM SIGPLAN 85 Symposium on Language Issues in Programming Environments. Number 7 in SIGPLAN Notices 20. ACM, New York, pp. 131--139.

[15]

Gries, D. and Volpano, D. 1990. The transform---A new language construct. Struct. Prog. 11, 1, 1--10.

[16]

Hoare, C. A. R. 1972. Proof of correctness of data representations. Acta Inf. 1, 4, 271--81.

[17]

Hoare, C. A. R. and Wirth, N. 1973. An axiomatic definition of the programming language PASCAL. Acta Inf. 2, 4, 335--355.

[18]

Hogg, J. 1991. Islands: Aliasing protection in object-oriented languages. In Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '91), A. Paepcke, Ed. Number 11 in SIGPLAN Notices 26. ACM, New York, pp. 271--285.

[19]

Jackson, D. 1995. Aspect: Detecting bugs with abstract dependences. ACM Trans. Softw. Eng. Meth. 4, 2 (Apr.), 109--145.

[20]

Jones, C. B. 1986. Systematic Software Development using VDM. International Series in Computer Science. Prentice-Hall, Englewood Cliffs, N.J.

[21]

Jonkers, H. B. M. 1991. Upgrading the pre- and postcondition technique. In VDM '91 Formal Software Development Methods: 4th International Symposium of VDM Europe. Volume 1: Conference Contributions, S. Prehn and W. J. Toetenel, Eds. Lecture Notes in Computer Science, vol. 551. Springer-Verlag, New York, pp. 428--456.

[22]

Joshi, R. 1997. Extended static checking of programs with cyclic dependencies. In 1997 SRC Summer Intern Projects, J. Mason, Ed. Technical Note 1997-028. Digital Equipment Corporation Systems Research Center.

[23]

Lamport, L. and Schneider, F. B. 1985. Constraints: A uniform approach to aliasing and typing. In Conference Record of the 12th Annual ACM Symposium on Principles of Programming Languages. ACM, New, York, pp. 205--216.

[24]

Leavens, G. T. 1996. An overview of Larch/C++: Behavioral specifications for C++ modules. In Specification of Behavioral Semantics in Object-Oriented Information Modeling, H. Kilov and W. Harvey, Eds. Kluwer Academic Publishers, Chapter 8, 121--142.

[25]

Leavens, G. T., Baker, A. L., and Ruby, C. 1999. Preliminary design of JML: A behavioral interface specification language for Java. Tech. Rep. 98-06f. Department of Computer Science. Iowa State University, July. Available at ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/.

[26]

Leino, K. R. M. 1995. Toward reliable modular programs. Ph.D. dissertation, California Institute of Technology. Tech. Rep. Caltech-CS-TR-95-03.

[27]

Leino, K. R. M. 1997. Ecstatic: An object-oriented programming language with an axiomatic semantics. In Proceedings of the Fourth International Workshop on Foundations of Object-Oriented Languages. Proceedings available from http://www.cs.williams.edu/&sim;kim/FOOL/.

[28]

Leino, K. R. M. 1998a. Data groups: Specifying the modification of extended state. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '98). Number 10 in SIGPLAN Notices 33. ACM, New York, pp. 144--153.

[29]

Leino, K. R. M. 1998b. Recursive object types in a logic of object-oriented programs. Nord. J. Comput. 5, 4 (Winter), 330--360.

[30]

Leino, K. R. M. and Nelson, G. 2000. Data abstraction and information hiding. Research Rep. 160, Compaq Systems Research Center. Nov.

[31]

Leino, K. R. M., Nelson, G., and Saxe, J. B. 2000. ESC/Java user's manual. Tech. Note 2000-002, Compaq Systems Research Center. Oct.

[32]

Leino, K. R. M. and Stata, R. 1997. Checking object invariants. Tech. Note 1997-007, Digital Equipment Corporation Systems Research Center. Jan.

[33]

Leino, K. R. M. and Stata, R. 1999a. Smothering rep exposure with reads clauses. Internal manuscript KRML 90, Compaq Systems Research Center.

[34]

Leino, K. R. M. and Stata, R. 1999b. Virginity: A contribution to the specification of object-oriented software. Inf. Process. Lett. 70, 2 (Apr.), 99--105.

[35]

Liskov, B. and Guttag, J. 1986. Abstraction and Specification in Program Development. MIT Electrical Engineering and Computer Science Series. MIT Press, Cambridge Mass.

[36]

Milner, R. 1971. An algebraic definition of simulation between programs. Tech. Rep. Stanford Artificial Intelligence Project Memo AIM-142, Computer Science Department Report No. CS-205, Stanford Univ. Stanford, Calif., Feb.

[37]

Mitchell, J. G., Maybury, W., and Sweet, R. 1979. The Mesa language manual, version 5.0. Tech. Rep. CSL-79-3, Xerox PARC. Apr.

[38]

Morris, J. M. 1989. Laws of data refinement. Acta Inf. 26, 4 (Feb.), 287--308.

[39]

Mössenböck, H. and Wirth, N. 1991. The programming language Oberon-2. Struct. Prog. 12, 4, 179--195.

[40]

Müller, P. 2001. Modular specification and verification of object-oriented programs. Ph.D. dissertation, FernUniversität Hagen. Available from http://www.informatik.fernuni-hagen.de/pi5/publications.html.

[41]

Müller, P. and Poetzsch-Heffter, A. 2000. Modular specification and verification techniques for object-oriented software components. In Foundations of Component-Based Systems, G. T. Leavens and M. Sitaraman, Eds. Cambridge University Press, Chapter 7, 137--159.

[42]

Müller, P. and Poetzsch-Heffter, A. 2001. Universes: A type system for alias and dependency control. Tech. Rep. 279, FernUniversität Hagen. Available from http://www.informatik.fernuni-hagen.de/pi5/publications.html.

[43]

Nelson, G. 1983. Verifying reachability invariants of linked structures. In Conference Record of the 10th Annual ACM Symposium on Principles of Programming Languages. ACM, New York, pp. 38--47.

[44]

Nelson, G., Ed. 1991. Systems Programming with Modula-3. Series in Innovative Technology. Prentice-Hall, Englewood Cliffs, N.J.

[45]

Noble, J., Vitek, J., and Potter, J. 1998. Flexible alias protection. In ECOOP'98---Object-oriented Programming: 12th European Conference, E. Jul, Ed. Lecture Notes in Computer Science, vol. 1445. Springer-Verlag, New York, pp. 158--185.

[46]

Parnas, D. L. 1972. On the criteria to be used in decomposing systems into modules. Commun. ACM 15, 12 (Dec.), 1053--1058. Reprinted as http://www.acm.org/classics/may96/.

[47]

Stoy, J. E. and Strachey, C. 1972. OS6---An experimental operating system for a small computer. Part II: Input/output and filing system. Comput. J. 15, 3, 195--203.

[48]

Utting, M. 1995. Reasoning about aliasing. In Proceedings of the 4th Australasian Refinement Workshop (ARW-95). School of Computer Science and Engineering, The University of New South Wales, 195--211.

[49]

Wirth, N. 1977. Modula: A language for modular multiprogramming. Softw. Pract. Exper. 7, 1 (Jan.--Mar.), 3--35.

[50]

Wirth, N. 1982. Programming in Modula-2. Springer-Verlag, New York.

[51]

Wirth, N. 1988. The programming language Oberon. Softw. Pract. Exper. 18, 7 (July), 671--690.

Cited By

Bordis TCleophas LKittelmann ARunge TSchaefer IWatson B(2022)Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeYThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_5(80-104)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_5
Xie ATan D(2020)The Impact of Interaction on the Travel ArrangementProceedings of the 2nd International Electronics Communication Conference10.1145/3409934.3409954(150-154)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3409934.3409954
Astrauskas VMüller PPoli FSummers A(2019)Leveraging rust types for modular specification and verificationProceedings of the ACM on Programming Languages10.1145/33605733:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360573
Show More Cited By

Index Terms

Recommendations

Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement

Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an ...
Abstraction for conflict-free replicated data types
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Strong eventual consistency (SEC) has been used as a classic notion of correctness for Conflict-Free Replicated Data Types (CRDTs). However, it does not give proper abstractions of functionality, thus is not helpful for modular verification of client ...
An Interface Theory for Program Verification
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles
Abstract
Program verification is the problem, for a given program and a specification , of constructing a proof of correctness for the statement “program satisfies specification ” () or a proof of violation ([inline-graphic not available: see fulltext]). ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 24, Issue 5

September 2002

137 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/570886

Issue’s Table of Contents

Copyright © 2002 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2002

Published in TOPLAS Volume 24, Issue 5

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

104
Total Citations
View Citations
2,191
Total Downloads

Downloads (Last 12 months)193
Downloads (Last 6 weeks)20

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bordis TCleophas LKittelmann ARunge TSchaefer IWatson B(2022)Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeYThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_5(80-104)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_5
Xie ATan D(2020)The Impact of Interaction on the Travel ArrangementProceedings of the 2nd International Electronics Communication Conference10.1145/3409934.3409954(150-154)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3409934.3409954
Astrauskas VMüller PPoli FSummers A(2019)Leveraging rust types for modular specification and verificationProceedings of the ACM on Programming Languages10.1145/33605733:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360573
Song HMartínez JBedell PVennin NLefebvre S(2019)Colored Fused Filament FabricationACM Transactions on Graphics10.1145/318379338:5(1-11)Online publication date: 26-Jun-2019
https://dl.acm.org/doi/10.1145/3183793
Bao YLeavens GErnst G(2018)Unifying separation logic and region logic to allow interoperabilityFormal Aspects of Computing10.1007/s00165-018-0455-530:3-4(381-441)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0455-5
Pack CSon SShin S(2017)Computer aided diagnosis with boosted learning for anomaly detection in microwave tomographyACM SIGAPP Applied Computing Review10.1145/3161534.316153817:3(39-47)Online publication date: 14-Nov-2017
https://dl.acm.org/doi/10.1145/3161534.3161538
Khlif IKacem MEichler CKacem A(2017)A multi-scale modeling approach for systems of systems architecturesACM SIGAPP Applied Computing Review10.1145/3161534.316153617:3(17-26)Online publication date: 14-Nov-2017
https://dl.acm.org/doi/10.1145/3161534.3161536
Nguyễn PGilray TTobin-Hochstadt SVan Horn D(2017)Soft contract verification for higher-order stateful programsProceedings of the ACM on Programming Languages10.1145/31581392:POPL(1-30)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158139
Fragoso Santos JMaksimović PNaudžiūnienė DWood TGardner P(2017)JaVerT: JavaScript verification toolchainProceedings of the ACM on Programming Languages10.1145/31581382:POPL(1-33)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158138
Flückiger OScherer GYee MGoel AAhmed AVitek J(2017)Correctness of speculative optimizations with dynamic deoptimizationProceedings of the ACM on Programming Languages10.1145/31581372:POPL(1-28)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158137
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents