Data abstraction and information hiding

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
	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	John Boyland, Alias burying: unique variables without destructive reads, Software—Practice & Experience, v.31 n.6, p.533-553, May 2001 [doi>10.1002/spe.370]
	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	Margaret A. Ellis , Bjarne Stroustrup, The annotated C++ reference manual, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	9	G. W. Ernst , R. J. Hookway , W. F. Ogden, Modular Verification of Data Abstractions with Shared Realizations, IEEE Transactions on Software Engineering, v.20 n.4, p.288-307, April 1994 [doi>10.1109/32.277576]
	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	James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
	14	David Gries , Jan Prins, A new notion of encapsulation, Proceedings of the ACM SIGPLAN 85 symposium on Language issues in programming environments, p.131-139, June 25-28, 1985, Seattle, Washington, United States
	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	John Hogg, Islands: aliasing protection in object-oriented languages, Conference proceedings on Object-oriented programming systems, languages, and applications, p.271-285, October 06-11, 1991, Phoenix, Arizona, United States
	19	Daniel Jackson, Aspect: detecting bugs with abstract dependences, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.109-145, April 1995 [doi>10.1145/210134.210135]
	20	C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
	21	H. B. M. Jonkers, Upgrading the Pre- and Postcondition Technique, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.428-456, October 21-25, 1991
	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	Leslie Lamport , Fred B. Schneider, Constraints: a uniform approach to aliasing and typing, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.205-216, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318640]
	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	K. Rustan Leino, Toward reliable modular programs, California Institute of Technology, Pasadena, CA, 1995
	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/∼kim/FOOL/.
	28	K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
	29	K. Rustan M. Leino, Recursive object types in a logic of object-oriented programs, Nordic Journal of Computing, v.5 n.4, p.330-360, Winter 1998
	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	K. Rustan M. Leino , Raymie Stata, Virginity: a contribution to the specification of object-oriented software, Information Processing Letters, v.70 n.2, p.99-105, April 30, 1999 [doi>10.1016/S0020-0190(99)00043-5]
	35	Barbara Liskov , John Guttag, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
	36	Robin Milner, An algebraic definition of simulation between programs, Stanford University, Stanford, CA, 1971
	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	J. M. Morris, Laws of data refinement, Acta Informatica, v.26 n.4, p.287-308, Feb. 1989
	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	Peter Müller , Arnd Poetzsch-Heffter, Modular specification and verification techniques for object-oriented software components, Foundations of component-based systems, Cambridge University Press, New York, NY, 2000
	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	Greg Nelson, Verifying reachability invariants of linked structures, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-47, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567073]
	44	Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
	45	James Noble , Jan Vitek , John Potter, Flexible Alias Protection, Proceedings of the 12th European Conference on Object-Oriented Programming, p.158-185, July 20-24, 1998
	46	D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
	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	Niklaus Wirth, Programming in MODULA-2 (3rd corrected ed.), Springer-Verlag New York, Inc., New York, NY, 1985
	51	N. Wirth, The programming language Oberon, Software—Practice & Experience, v.18 n.7, p.671-690, July 1988 [doi>10.1002/spe.4380180707]