|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| Murali Sitaraman, Bruce W. Weide, William F. Ogden, "On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations," IEEE Transactions on Software Engineering, vol. 23, no. 3, pp. 157-170, March, 1997. | |||
| BibTex | x | ||
| @article{ 10.1109/32.585503, author = {Murali Sitaraman and Bruce W. Weide and William F. Ogden}, title = {On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations}, journal ={IEEE Transactions on Software Engineering}, volume = {23}, number = {3}, issn = {0098-5589}, year = {1997}, pages = {157-170}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.585503}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Software Engineering TI - On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations IS - 3 SN - 0098-5589 SP157 EP170 EPD - 157-170 A1 - Murali Sitaraman, A1 - Bruce W. Weide, A1 - William F. Ogden, PY - 1997 KW - Abstract data type KW - abstraction function KW - abstraction mapping KW - abstraction relation KW - data abstraction KW - formal specification KW - greedy algorithm KW - program verification KW - nondeterminism KW - optimization problem KW - relation. VL - 23 JA - IEEE Transactions on Software Engineering ER - | |||
Abstract—The typical correspondence between a concrete representation and an abstract conceptual value of an abstract data type (ADT) variable (object) is a many-to-one function. For example, many different pointer aggregates give rise to exactly the same binary tree. The theoretical possibility that this correspondence generally should be relational has long been recognized. By using a nontrivial ADT for handling an optimization problem, we show why the need for generalizing from functions to relations arises naturally in practice. Making this generalization is among the steps essential for enhancing the practical applicability of formal reasoning methods to industrial-strength software systems.
[1] M. Abadi and L. Lamport, "The Existence of Refinement Mappings," Theoretical Computing Science, vol. 82, no. 2, pp. 253-284, May 1991.
[2] A. Bloesch, E. Kazmierczak, P. Kearney, and O. Traynor, "Cogito: A Methodology and System for Formal Software Development," Intl. J. Software Eng. and Knowledge Eng., vol. 5, no. 4 pp. 599-617, Dec. 1995.
[3] S.A. Cook, "Soundness and Completeness of an Axiom System for Program Verification," SIAM J. Computing, vol. 7, no. 1, pp. 70-90, Feb. 1978.
[4] T.H. Cormen,C.E. Leiserson, and R.L. Rivest,Introduction to Algorithms.Cambridge, Mass.: MIT Press/McGraw-Hill, 1990.
[5] H.-D. Ehrich and A. Sernadas, "Algebraic Implementation of Objects over Objects," Stepwise Refinement of Distributed Systems—Lecture Notes in Computer Science 430.New York: Springer-Verlag, pp. 239-266, 1990.
[6] G.W. Ernst, R.J. Hookway, J.A. Menegay, and W.F. Ogden, "Modular Verification of Ada Generics," Computer Language, vol. 16, nos. 3/4, pp. 259-280, 1991.
[7] G.W. Ernst, R.J. Hookway, and W.F. Ogden, "Modular Verification of Data Abstractions with Shared Realizations," IEEE Trans. Software Eng. vol. 20, no. 4, pp. 288-307, Apr. 1994.
[8] D.E. Harms and B.W. Weide, "Copying and Swapping: Influences on the Design of Reusable Software Components," IEEE Trans. Software Eng., vol. 17, no. 5, pp. 424-435, May 1991.
[9] J. He, C.A.R. Hoare, and J.W. Sanders, "Data Refinement Refined," Lecture Notes in Computer Science 213, B. Robinet and R. Wilhelm, eds., pp. 187-196, Springer-Verlag.
[10] C.A.R. Hoare, "Proof of Correctness of Data Representations," Acta Informatica, vol. 1, no. 1, pp. 271-281, 1972; also in D. Gries, ed., Programming Methodology: A Collection of Articles by Members of IFIP WG 2.3, pp. 269-281,New York: Springer-Verlag, 1978.
[11] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: Prentice-Hall, 1990, 2nd ed.
[12] D. Kapur and S. Mandayam, "Expressiveness of the Operation Set of a Data Abstraction," Conf. Record Seventh Ann. ACM Symp. Principles of Programming Languages, pp. 139-153, ACM, 1980.
[13] G. Leavens, "Modular Specification and Verification of Object-Oriented Programs," IEEE Software, Nov./Dec., 1991, pp. 72-80.
[14] B.H. Liskov and J.M. Wing, "A New Definition of the Subtype Relation," ECOOP'93—Object-Oriented Programming, Proc. Seventh European Conf, Lecture Notes in Computer Science, vol. 707, pp. 118-141,New York: Springer-Verlag, 1993.
[15] B. Liskov and J.M. Wing, "Corrigenda to ECOOP '93 Paper," ACM SIGPLAN Notices, vol. 29, no. 4, p. 4, Apr. 1994.
[16] N. Lynch, "Multivalued Possibilities Mappings," Stepwise Refinement of Distributed Systems—Lecture Notes in Computer Science 430, pp. 519-543,New York: Springer-Verlag, 1990.
[17] G. Nelson, "A Generalization of Dijkstra's Calculus," ACM Trans. on Program Languages and Systems, vol. 11, no. 4, pp. 517-561, Oct. 1989.
[18] T. Nipkow, "Are Homomorphisms Sufficient for Behavioral Implementations of Deterministic and Nondeterministic Data Types?" Lecture Notes in Computer Science 247, F.J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, eds., pp. 260-271,New York: Springer-Verlag, 1987.
[19] O. Schoett, "Behavioral Correctness of Data Representations," Science of Computer Programming, vol. 14, pp. 43-57, 1990.
[20] M. Sitaraman, L.R. Welch, and D.E. Harms, "On Specification of Reusable Software Components," Intl. J. Software Eng. and Knowledge Eng., vol. 3, no. 2, pp. 207-219, June 1993.
[21] M. Sitaraman and B. Weide, "Component-Based Software Using RESOLVE," ACM Software Eng. Notes, Oct. 1994.
[22] M. Sitaraman, "Impact of Performance Considerations on Formal Specification Design," Formal Aspects of Computing, vol. 8, no. 6, pp. 716-736, 1997.
[23] B.W. Weide and J.E. Hollingsworth, "Scalability of Reuse Technology to Large Systems Requires Local Certifiability," Proc. Fifth Ann. Workshop Software Reuse,Palo Alto, Calif., Oct. 1992.
[24] B.W. Weide and W.F. Ogden, “Recasting Algorithms to Encourage Reuse,” IEEE Software, vol. 11, no. 5, Sept. 1994.
[25] B.W. Weide, S.H. Edwards, W.D. Heym, T.J. Long, and W.F. Ogden, "Characterizing Observability and Controllability of Software Components," Proc. Fourth Int'l Conf. Software Reuse, M. Sitaraman, ed., pp. 62-71, IEEE, Apr. 1996.
[26] J.M. Wing, “A Specifier's Introduction to Formal Methods,” IEEE Computer, vol. 23, pp. 8–24, Sept. 1990.