This Article 
 Bibliographic References 
 Add to: 
Modular Verification of Data Abstractions with Shared Realizations
April 1994 (vol. 20 no. 4)
pp. 288-307

Presents a method for the modular specification and verification of data abstractions in which multiple abstract objects share a common realization level data structure. Such shared realizations are an important implementation technique for data abstractions, because they provide for efficient use of memory; i.e., they allow the amount of memory allocated to the realization of an abstract object to be dynamic, so that only the amount of memory needed for its realization is allocated to it at any one time. To be explicit, an example of this kind of data abstraction is given. Although a number of programming languages provide good support for shared realizations, there has been limited research on its specification and verification. An important property of The authors' method is that it allows data abstractions to be dealt with modularly; i.e., each data abstraction can be specified and verified individually. Its abstract specification is made available for use by other program modules, but all of its implementation details are hidden, which simplifies the verification of code that uses the abstraction. The authors have developed semantics for data abstractions and their method of specification, and have used it to prove that their verification method is logically sound and relatively complete in the sense of Cook (1978). The use of shared realizations impacts specification and verification in several related ways. The manipulation of one abstract object may inadvertently produce a side effect on other abstract objects. Without shared realizations, such unwanted side effects can be prevented by scoping rules, but this is not possible with shared realizations. Instead, the absence of such side effects must be explicitly proven by the verification method. This requires the specification language to provide for quantification over the currently active (allocated) instances of an abstract type that is not necessary for the specification of less advanced implementations of data abstractions.

[1] U.S. Department of Defense,Reference Manual for the Ada Programming Language, ANSI/MIL-STD-1815A-1983, Dec. 1983.
[2] R. J. R. Back, "A calculus of program derivations,"Acta Informatica, vol. 25, pp. 593-624, 1988.
[3] B. Belkhouche and J. E. Urban, "Direct implementation of abstract data type from abstract specifications,"IEEE Trans. Software Eng., vol. SE- 12, pp. 649-661, May 1986.
[4] F.J.H. Boinck and H. van Tilborg, "Constructions and bounds for systematictEC/AUED codes,"IEEE Trans. Inform. Theory, vol. IT-36, pp. 1381-1390, Nov. 1990.
[5] E. Chang, N.E. Kaden, and W.D. Elliott, "Abstract data types in Euclid,"SIGPLAN Notices, vol. 13, no. 3, pp. 34-42, Mar. 1978.
[6] E.M. Clarke, "Programming language constructs for which it is impossible to obtain good Hoare axiom systems,"J. ACM., vol. 26, no. 1, pp. 129-147, Jan. 1979.
[7] S.A. Cook, "Soundness and completeness of an axiom system for program verification,"SIAM J. Computing., vol. 7, pp. 70-90, Feb. 1978.
[8] O.J. Dahl, B. Myhrhaug, and K. Nygaard, "The SIMULA 67 common base language," Pub. S-22, Norwegian Computing Center, Oslo, Norway, 1970.
[9] J.E. Donahue, "Complementary definitions of programming language semantics," Tech. Rep. CSRG-62, Comput. Syst. Res. Group, Univ. of Toronto, ON, Canada, Nov. 1975.
[10] H. Ehrig, "Algebraic implementation of abstract data types: Concept, syntax, semantics and correctness,"Lecture Notes in Computer Science: Automata, Languages and Programming, vol. 85, pp. 142-156, 1980.
[11] Ehrig, H., and B. Mahr,Fundamentals of Algebraic Specification 1, Springer-Verlag, Berlin, 1985.
[12] G.W. Ernst, R.J. Hookway, J.A. Menegay, and W.F. Ogden, "Modular verification of Ada generics,"Comput. Languages, vol. 16, pp. 259-280, 1991.
[13] G.W. Ernst, R.J. Hookway, J.A. Menegay, and W.F. Ogden, "Semantics of programming languages for modular verification," Tech. Rep. CES-85-4, Dept. Comput. Eng. and Sci., Case Western Reserve Univ., Cleveland, OH, 1985.
[14] G.W. Ernst, R.J. Hookway, and W.F. Ogden, "Modular verification of data abstraction in Modula-2," Tech. Rep. CES-89-10, Dept. of Comput. Eng. and Sci., Case Western Reserve Univ., Cleveland, OH, 1989.
[15] G.W. Ernst and W.F. Ogden, "Specification of abstract data types in Modula,"ACM Trans. Programming Languages Syst., vol. 2, no. 4, pp. 522-534, Oct. 1980.
[16] J.D. Gannon, R.G. Hamlet, and H.D. Mills, "Theory of modules,"IEEE Trans. Software Eng., vol. 14, no. 7, pp. 820-829, July 1987.
[17] S.L. Gerhart, D.R. Musser, D.H. Thompson, D.A. Baker, R.L. Bates, R.W. Erickson, R.L. London, D.G. Taylor, and D.S. Wile, "An overview of AFFIRM: A specification and verification system,"Inform. Processing. Amsterdam: North-Holland, pp. 343-347, 1980.
[18] C. M. Geschke, J. H. Morris, and E. H. Satterthwaite, "Early experience with Mesa,"Commun. ACM, vol. 20, (Tech. Rep. 8,) pp. 540-553, Aug. 1977.
[19] A. Goldberg and D. Robson,Smalltalk-80: The Language. Reading, MA: Addison-Wesley, 1989.
[20] G.A. Gorelick, "A complete axiomatic system for proving assertions about recursive and non-recursive programs," Tech. Rep. 75, Dept. of Comput. Sci., Univ. of Toronto, ON, Feb. 1975.
[21] J. Grabowski and P. Lescanne, "Modular algebraic specifications,"Mathematical Research: Algebraic and Logic Programming, Berlin: Akademie-Verlag, 1989, pp. 168-179.
[22] D. Gries and D. Volpano, "The transform: A new language construct,"Structured Programming, vol. 11, pp. 1-10, 1990.
[23] J. Guttag, J.J. Horning and J.M. Wing, "The Larch family of specification languages,"IEEE Software, vol. 2, no. 5, pp. 24-36, 1985.
[24] J. V. Guttag, E. Horowitz, and D. R. Musser, "Abstract data types and software validation,"Commun. ACM, vol. 21, pp. 1048-1064, Dec. 1978.
[25] B. Hailpern and S.S. Owicki, "Modular verification of concurrent programs,"Symp. Principles Programming Languages, 1982, pp. 322-336.
[26] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[27] C.A.R Hoare, "Proof of correctness of data representations,"Acta Informatica, vol. 1, pp. 271-281, 1972.
[28] S. Igarashi, R.L. London, and D. Luckham, "Automatic program verification I: A logical basis and its implementation,"Acta Informatica, vol. 4, pp. 145-182, 1975.
[29] P. Jalote, "Synthesizing implementations of abstract data types from axiomatic specifications,"Software: Practice and Experience, vol. 17, no. 11, pp. 847-858, Nov. 1987.
[30] R.A. Kemmerer, "A critique of the Gypsy verification system,"Verification Assessment Study, Final Report, The Gypsy System, Vol. II, R. A. Kemmerer, Ed. Fort George G. Meade, MD: National Computer Security Center, 1986, pp. 49-61.
[31] B.W. Lampson, J.J. Horning, R.L. London, J.G. Mitchell and G.J. Popek, "Report on the programming language Euclid,"SIGPLAN Notices, vol. 12, no. 2, pp. 1-79, Feb. 1977.
[32] B. Liskov and J. Guttag,Abstraction and Specification in Program Development. Cambridge, MA: MIT Press, 1986.
[33] R.L. London, J. V. Guttag, J. J, Horning, B. W. Lampson, J. G. Mitchell, and G.J. Popek, "Proof rules for the programming language Euclid,"Acta Informatica, vol. 10, pp. 1-26, Jan. 1978.
[34] D.C. Luchkam and W. Polak, "A practical method of documenting and verifying Ada programs with packages,"Proc. ACM-SIGPLAN Symp. Ada Programming Language, 1980, pp. 113-122.
[35] D. C. Luckham, F. W. von Henke, B. Krieg-Brückner, and O. Owe,ANNA, A Language for Annotating Ada Programs(Lecture Notes in Computer Science, Vol. 260). New York: Springer-Verlag, 1987.
[36] G. Nelson, "A generalization of Dijkstra's calculus,"ACM Trans. Programming Languages Syst., vol. 11, pp. 517-561, Oct. 1989.
[37] B. Meyers,Object Oriented Software Construction. Englewood Cliffs, NJ: Prentice-Hall, 1988.
[38] J. M. Morris, "Laws of data refinement,"Acta Informatica, vol. 26, pp. 287-308, 1989.
[39] D.R. Musser, "On proving inductive properties of abstract data types,"3rd ACM Symp. Principles of Programming Languages, 1980, pp. 154-162.
[40] E.R. Olderog, "Sound and complete Hoare-like calculi based on copy rules,"Acta Informatica, vol. 16, pp. 161-197, 1981.
[41] D.C. Oppen and S.A. Cook, "Proving assertions about programs that manipulate data structures,"Proc. 7th Ann. ACM Symp. Theory of Computing, 1975, pp. 107-116.
[42] D. Scott and C. Strachey, "Toward a mathematical semantics for computer languages,"Computers and Automation. New York: Wiley, 1972, pp. 19-46.
[43] D. Scott, "Some definitional suggestions for automata theory,"J. Comput. Syst. Sci., vol. 1, pp. 187-212, 1967.
[44] J. Spitzen and B. Wegbreit, "The verificaiion and synthesis of data structures,"Acta Informatica, vol. 4, pp. 127-144, 1975.
[45] A. Stoughton, "Substitution revisited,"Theoretical Comput. Sci., vol. 59, pp. 317-325, 1988.
[46] B. Stroustrup,The C++ Programming Language. Reading, MA: Addison-Wesley, 1986.
[47] M. Wand, "Specifications, models, and implementation of data structures,"Theoretical Comput. Sci., vol. 20, pp. 3-32, 1982.
[48] N. Wirth,Programming in Modula-2, 3rd ed. Berlin: Springer-Verlag, 1985.
[49] W.A. Wulf, R.L. London, and M. Shaw, "An introduction to the construction and verification of Alphard programs,"IEEE Trans. Software Eng., vol. 2, no. 12, pp. 253-264, Dec. 1976.
[50] W.D. Young and D.I. Good, "Generics and verification in Ada,"Proc. ACM-SIGPLAN Symp. Ada Programming Language, 1980, pp. 123-127.

Index Terms:
data structures; program verification; specification languages; modular verification; data abstractions; shared realizations; modular specification; realization level data structure; abstract specification; semantics; quantification
G.W. Ernst, R.J. Hookway, W.F. Ogden, "Modular Verification of Data Abstractions with Shared Realizations," IEEE Transactions on Software Engineering, vol. 20, no. 4, pp. 288-307, April 1994, doi:10.1109/32.277576
Usage of this product signifies your acceptance of the Terms of Use.