Program verifications, object interdependencies, and object types

• Autorzy: Xing C. C.
• Języki publikacji: EN

Abstrakty

EN

Object types are abstract specifications of object behaviors; object behaviors are abstractly indicated by object component interdependencies; and program verifications are based on object behaviors. In conventional object type systems, object component interdependencies are not taken into account. As a result, distinct behaviors of objects are confused in conventional object type systems, which can lead to fundamental typing/subtyping loopholes and program verification troubles. In this paper, we first identify a program verification problem which is caused by the loose conventional object typing/subtyping which is in turn caused by the overlooking of object component interdependencies. Then, as a new object typing scheme, we introduce object type graphs (OTG) in which object component interdependencies are integrated into object types. Finally, we show how the problem existing in conventional object type systems can be easily resolved under OTG.

Słowa kluczowe

EN

object type; Object-Oriented Language; object-oriented programming

• Wydawca: Oficyna Wydawnicza Politechniki Wrocławskiej
• Czasopismo: e-Informatica Software Engineering Journal
• Rocznik: 2007
• Tom: Vol. 1, nr 1
• Strony: 77--97
• Opis fizyczny: Bibliogr. 22 poz.

Twórcy

autor

Xing C. C.

• Department of Mathematics and Computer Science, Nicholls State University

Bibliografia

• [1] http://caml.inria.fr/ocaml/. 2007.
• [2] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, New York, 1996.
• [3] V. Bono, M. Bugliesi, M. Dezani-Ciancaglini, and L. Liquori. Subtyping for Extensible,Incompete objects. Fundamenta Informaticae, 38(4):325–364, 1999.
• [4] V. Bono and L. Liquori. A subtyping for the Fisher-Honsell-Mitchell lambda calculus of objects. In Proc. of International Conference of Computer Science Logic, number 933 in LNCS, pages 16–30. 1995.
• [5] K. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2):127–206, 1994.
• [6] K. Bruce. Foundations of Object-Oriented Languages. MIT Press, 2002.
• [7] K. Bruce, A. Schuett, R. van Gent, and A. Fiech. Polytoil: A type-safe polymorphic objectoriented language. ACM Transactions on Programming Languages and Systems, 25(2):225–290, 2003.
• [8] W. Cook, W. Hill, and P. Canning. Inheritance is not subtyping. In Proceedings of the 17the Annual ACM Symposium on Principles of Programming Languages, pages 125–135, 1990.
• [9] R. Deline and M. Fahndrich. Typestates for objects. In ECOOP 2004, 2004.
• [10] H. Ehrig. Introduction to the algebraic theory of graph grammars. In Graph-Grammars and Their Applications to Computer Science and Biology, volume 73 of Lecture Notes in Computer Science, pages 1–69. Springer-Verlag, 1978.
• [11] H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozenberg, editors. Handbook of Graph Grammars and Computing by Graph Transformation, volume 2. World Scientific, 1999.
• [12] H. Ehrig, H.-J. Kreowski, U. Montanari, and G. Rozenberg, editors. Handbook of Graph Grammars and Computing by Graph Transformation, volume 3. World Scientific, 1999.
• [13] H. Ehrig, M. Pfender, and H. J. Schneider. Graph grammars: An algebraic approach. In IEEE Conference of Automata and Switching Theory, pages 167–180, 1973.
• [14] K. Fisher, F. Honsell, and J. Mitchell. A lambda calculus of objects and method specialization.Nodic Journal of Computing, 1:3–37, 1994.
• [15] J. Hickey. Introduction to OCaml, http://caml.inria.fr/tutorials-eng.html. 2002.
• [16] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM,12:576–580, 1969.
• [17] M. Huth and M. Ryan. Logic in Computer Science. Cambridge University Press, 2nd edition, 2004.
• [18] L. Liquori. On object extension. In ECOOP’98 Object-oriented Programming, number 1445 in Lecture Notes in Computer Science, pages 498–522. Springer–Verlag, 1998. Program Verifications, Object Interdependencies, and Object Types 97
• [19] L. Liquori and G. Castagna. A Typed Lambda Calculus of Objects. Number 1179 in Lecture Notes in Computer Science, pages 129–141. Springer–Verlag, 1996.
• [20] B. Liskov and J. Wing. A Behavioral Notion of Subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811–1841, 1994.
• [21] O. L. Madsen. Towards Integration of State Machines and Object-Oriented Languages. In Technology of Object-Oriented Languages and Systems (TOOLS Europe’99), 1999.
• [22] G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformation, volume 1. World Scientific, 1997