Abstract
This paper develops a mathematical characterisation of object-oriented concepts by defining an observation-oriented semantics for an object-oriented language (OOL) with a rich variety of features including subtypes, visibility, inheritance, dynamic binding and polymorphism. The language is expressive enough for the specification of object-oriented designs and programs. We also propose a calculus based on this model to support both structural and behavioural refinement of object-oriented designs. We take the approach of the development of the design calculus based on the standard predicate logic in Hoare and He’s Unifying Theories of Programming (UTP). We also consider object reference in terms of object identity as values and mutually dependent methods.
The work is supported by the 211 Key Project of MoE and the 973 Project 2002CB312001 of MoST of China.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardeli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Abadi, M., Leino, R.: A logic of object-oriented programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997, pp. 682–696. Springer, Heidelberg (1997)
Abraham-Mumm, E., de Boer, F.S., de Roever, W.P., Steffen, M.: Verification for Java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol. 2303, pp. 5–20. Springer, Heidelberg (2002)
America, P.: Designing an object-oriented programming language with behavioural subtyping. In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol. 489, pp. 60–90. Springer, Heidelberg (1991)
America, P., de Boer, F.: Reasoning about dynamically evolving process structures. Formal Aspects of Computing 6(3), 269–316 (1994)
Bonsangue, M.M., Kok, J.N., Sere, K.: An approach to object-orientation in action systems. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 68–95. Springer, Heidelberg (1998)
Broy, M.: Object-oriented programming and software development - a critical assessment. In: McIver, A., Morgan, C. (eds.) Programming Methodology. Springer, Heidelberg (2003)
Carrington, D., et al.: Object-Z: an Object-Oriented Extension to Z. North-Holland, Amsterdam (1989)
Cavalcanti, A., Naumann, D.: A weakest precondition semantics for an object-oriented language of refinement. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1439–1460. Springer, Heidelberg (1999)
Coleman, D., et al.: Object-Oriented Development: the FUSION Method. Prentice-Hall, Englewood Cliffs (1994)
Cook, S., Daniels, J.: Designing Object Systems: Object-Oriented Modelling with Syntropy. Prentice-Hall, Englewood Cliffs (1994)
Dürr, E., Dusink, E.M.: The role of VDM + + in the development of a real-time tracking and tracing system. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670. Springer, Heidelberg (1993)
Fowler, M., Beck, K., Brant, J., Opdyke, W., Roberts, D.: Refactoring: Improving the Design of Existing Code. Addison-Wesley, Reading (1999)
Gamma, E., et al.: Design Patterns. Addison-Wesley, Reading (1995)
He, J., Liu, Z., Li, X.: Towards a refinement calculus for object-oriented systems (invited talk). In: Proc. ICCI 2002, Alberta, Canada. IEEE Computer Society Press, Los Alamitos (2002)
He, J., Liu, Z., Li, X.: A component calculus. In: Van, H.D., Liu, Z. (eds.) Proc. Of FME 2003 Workshop on Formal Aspects of Component Software (FACS 2003), UNU/IIST Technical Report 284, UNU/IIST, P.O. Box 3058, Macao, Pisa, Italy (2003)
He, J., Liu, Z., Li, X.: Contract-oriented component software development. Technical Report 276, UNU/IIST, P.O. Box 3058, Macao SAR China (2003)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Houston, I.: Formal specification of the OMG core object model. Technical report, IMB, UK, Hursely Park (1994)
Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)
Lano, K., Haughton, H.: Object-oriented specification case studies. Prentice Hall, New York (1994)
Larman, C.: Applying UML and Patterns. Prentice-Hall International, Englewood Cliffs (2001)
Rustan, K., Leino, M.: Recursive object types in a logic of object-oriented programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, p. 170. Springer, Heidelberg (1998)
Liu, Z.: Object-oriented software development in UML. Technical Report UNU/IIST Report No. 228, UNU/IIST, P.O. Box 3058, Macau, SAR, P.R. China (March 2001)
Liu, Z., He, J., Li, X., Chen, Y.: A relational model for formal requirements analysis in UML. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 641–664. Springer, Heidelberg (2003)
Liu, Z., He, J., Li, X., Liu, J.: Unifying views of UML. Research Report 288, UNU/IIST, P.O. Box 3058, Macao (2003); Presented at UML 2003 Workshop on Compostional Verification of UML and submitted for the inclusion in the final proceedings
Meyer, B.: From structured programming to object-oriented design: the road to Eiffel. Structured Programming 10(1), 19–39 (1989)
Mikhajlova, A., Sekerinski, E.: Class refinement and interface refinement in object-orient programs. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313. Springer, Heidelberg (1997)
Naumann, D.: Predicate transformer semantics of an Oberon-like language. In: Olerog, E.-R. (ed.) Proc. of PROCOMET 1994. North-Holland, Amsterdam (1994)
Pierik, C., de Boer, F.S.: A syntax-directed hoare logic for object-oriented programming concepts. Technical Report UU-CS-2003-010, Institute of Information and Computing Science, Utrecht University (2003)
Poetzsch-Heffter, A., Muller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)
Qin, S., Dong, J.S., Chin, W.N.: A semantics foundation for TCOZ in Unifying Theories of Programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 321–340. Springer, Heidelberg (2003)
Sekerinski, E.: A type-theoretical basis for an object-oriented refinement calculus. In: Proc. of Formal Methods and Object Technology. Springer, Heidelberg (1996)
Sherif, A., He, J.: Towards a time model for Circus. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, p. 613. Springer, Heidelberg (2002)
von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience 13(13), 1173–1214 (2001)
Woodcock, J.C.P., Cavalcanti, A.L.C.: A semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 184. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jifeng, H., Liu, Z., Li, X., Qin, S. (2004). A Relational Model for Object-Oriented Designs. In: Chin, WN. (eds) Programming Languages and Systems. APLAS 2004. Lecture Notes in Computer Science, vol 3302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30477-7_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-30477-7_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23724-2
Online ISBN: 978-3-540-30477-7
eBook Packages: Springer Book Archive