×

rCOS: a refinement calculus of object systems. (English) Zbl 1118.68049

Summary: A mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioural refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He’s Unifying Theories of Programming (UTP).

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q55 Semantics in the theory of computing

Software:

Circus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Leino, R., A logic of object-oriented programs, (Bidoit, M.; Dauchet, M., TAPSOFT ’97Theory and Practice of Software Development Seventh International Joint Conference (1997), Springer: Springer Berlin), 682-696
[2] Abraham-Mumm, E.; de Boer, F. S.; de Roever, W. P.; Steffen, M., Verification for Java’s reentrant multithreading concept, (Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Vol. 2303 (2002), Springer: Springer Berlin), 5-20 · Zbl 1077.68552
[3] P. America, Designing an object-oriented programming language with behavioural subtyping. in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), REX Workshop, Lecture Notes in Computer Science, Vol. 489, Springer, 1991, pp. 60-90.; P. America, Designing an object-oriented programming language with behavioural subtyping. in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), REX Workshop, Lecture Notes in Computer Science, Vol. 489, Springer, 1991, pp. 60-90.
[4] America, P.; de Boer, F., Reasoning about dynamically evolving process structures, Formal Aspects Comput., 6, 3, 269-316 (1994) · Zbl 0821.68106
[5] Back, R.; Mikhajlova, A.; von Wright, J., Class refinement as semantics of correct object substitutability, Formal Aspects Comput., 2, 18-40 (2000) · Zbl 0963.68103
[6] Back, R.; vonWright, J., Refinement Calculus (1998), Springer: Springer Berlin
[7] Back, R. J.R.; Petre, L.; Paltor, I. P., Formalizing UML use cases in the refinement calculus, (Proc. UML’99 (1999), Springer: Springer Berlin)
[8] Bonsangue, M. M.; Kok, J. N.; Sere, K., An approach to object-orientation in action systems, (Jeuring, J., Mathematics of Program Construction, Lecture Notes in Computer Science, Vol. 1422 (1998), Springer: Springer Berlin), 68-95
[9] Booch, G.; Rumbaugh, J.; Jacobson, I., The Unified Modelling Language User Guide (1999), Addison-Wesley: Addison-Wesley Berlin, MA
[10] Borba, P.; Sampaio, A.; Cornélio, M., A refinment algebra for object-oriented programming, (cardelli, L., Proc. ECOOP03, Lecture Notes in Computer Science, Vol. 2743 (2003), Springer: Springer Berlin), 457-482
[11] Broy, M., Object-oriented programming and software development—a critical assessment, (McIver, A.; Morgan, C., Programming Methodology (2003), Springer: Springer Berlin)
[12] Bruce, K.; Grabtre, J.; Kanapathy, G., An operational semantics for TOOPLE: a statically-typed object-oriented programming language, (Brooks, S.; etal., Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Vol. 802 (1994), Springer: Springer Berlin), 603-626 · Zbl 1509.68033
[13] Cavalcanti, A.; Naumann, D., A weakest precondition semantics for an object-oriented language of refinement, (Lecture Notes in Computer Science, Vol. 1709 (1999), Springer: Springer Berlin), 1439-1460 · Zbl 0953.68081
[14] Y. Chen, J. Sanders, Compositional reasoning for pointer structures, in: Eighth Internat. Conf. on Mathematics of Program Construction (MPC’06), Lecture Notes in Computer Science, Vol. 4014, Springer, Berlin, 2006, pp. 115-139.; Y. Chen, J. Sanders, Compositional reasoning for pointer structures, in: Eighth Internat. Conf. on Mathematics of Program Construction (MPC’06), Lecture Notes in Computer Science, Vol. 4014, Springer, Berlin, 2006, pp. 115-139. · Zbl 1235.68050
[15] Coleman, D., Object-Oriented Development: the FUSION Method (1994), Prentice-Hall: Prentice-Hall Englewood cliffs, NJ
[16] Cook, S.; Daniels, J., Designing Object Systems: Object-Oriented Modelling with Syntropy (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0841.68029
[17] Dürr, E.; Dusink, E. M., The role of \(VDM^{++}\) in the development of a real-time tracking and tracing system, (Woodcock, J.; Larsen, P., Proc. of FME’93, Lecture Notes in Computer Science, Vol. 670 (1993), Springer: Springer Berlin)
[18] Fowler, M.; Beck, K.; Brant, J.; Opdyke, W.; Roberts, D., Refactoring: Improving the Design of Existing Code (1999), Addison-Wesley: Addison-Wesley Reading, MA
[19] Fowler, M., Refectoring Improving the Design of Existing Code (2000), Addison-Wesley: Addison-Wesley Reading, MA
[20] Gamma, E.; Helm, R.; Johnson, R.; Vlissides, J., Design Patterns, Elements of Reusable Object-Oriented Software (1994), Addison-Wesley: Addison-Wesley Reading, MA
[21] Gamma, E., Design Patterns (1995), Addison-Wesley: Addison-Wesley Reading, MA
[22] D. Harel, B. Rumpe, Modeling languages: syntax, semantics and all that stuff—part I: the basic stuff, Technical Report MCS00-16, The Weizmann Institute of Science, Israel, September 2000.; D. Harel, B. Rumpe, Modeling languages: syntax, semantics and all that stuff—part I: the basic stuff, Technical Report MCS00-16, The Weizmann Institute of Science, Israel, September 2000.
[23] He, J.; Li, X.; Liu, Z., Component-based software engineering, (in: Proc. Second Internat. Colloq. on Theoretical Aspects of Computing (ICTAC05), Lecture Notes in Computer Science, Vol. 3722 (2005), Springer: Springer Berlin), 70-95 · Zbl 1169.68366
[24] He, J.; Liu, Z.; Li, X., Towards a refinement calculus for object-oriented systems (invited talk), (Proc. ICCI02, Alberta, Canada (2002), IEEE Computer Society: IEEE Computer Society Silverspring, MD)
[25] J. He, Z. Liu, X. Li, A theories of reactive contracts, Electronic Notes of Theoretical Computer Science, Vol. 160, 2006, pp. 173-195.; J. He, Z. Liu, X. Li, A theories of reactive contracts, Electronic Notes of Theoretical Computer Science, Vol. 160, 2006, pp. 173-195.
[26] J. He, Z. Liu, X. Li, S. Qin, A relational model of object oriented programs, in: Proc. of the Second ASIAN Symp. on Programming Languages and Systems (APLAS04), Lecture Notes in Computer Science, Vol. 3302, Taiwan, March 2004, Springer, Berlin, pp. 415-436.; J. He, Z. Liu, X. Li, S. Qin, A relational model of object oriented programs, in: Proc. of the Second ASIAN Symp. on Programming Languages and Systems (APLAS04), Lecture Notes in Computer Science, Vol. 3302, Taiwan, March 2004, Springer, Berlin, pp. 415-436. · Zbl 1116.68373
[27] Hoare, C. A.R., Laws for programming, Comm. ACM, 30, 672-686 (1987) · Zbl 0629.68006
[28] Hoare, C. A.R.; He, J., Unifying Theories of Programming (1998), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 1005.68036
[29] I. Houston, Formal specification of the OMG core object model, Technical Report, IMB, UK, Hursely Park, 1994.; I. Houston, Formal specification of the OMG core object model, Technical Report, IMB, UK, Hursely Park, 1994.
[30] Huisman, M.; Jacobs, B., Java program verification via a Hoare logic with abrupt termination, (Maibaum, T., FASE 2000, Lecture Notes in Computer Science, Vol. 1783 (2000), Springer: Springer Berlin), 284-303
[31] Jacobson, I.; Booch, G.; Rumbaugh, J., The Unified Software Development Process (1999), Addison-Wesley: Addison-Wesley Reading, MA
[32] Jin, N.; He, J., Resource models and pre-compiler specification for hardware/software, (Cuellar, J. R.; Liu, Z., Proc. Second Internat. Conf. on Software Engineering and Formal Methods SEFM04. Proc. Second Internat. Conf. on Software Engineering and Formal Methods SEFM04, Beijing, China (2004), IEEE Computer Society: IEEE Computer Society Sliverspring, MD), 28-30
[33] Kruchten, P., The Rational Unified Process—An Introduction (2000), Addison-Wesly: Addison-Wesly Reading, MA
[34] Lano, K.; Haughton, H., Object-oriented specification case studies (1994), Prentice-Hall: Prentice-Hall New York · Zbl 0827.68072
[35] Larman, C., Applying UML and Patterns (2001), Prentice-Hall International: Prentice-Hall International Englewood Cliffs, NJ
[36] Leino, K. R.M., Recursive object types in a logic of object-oriented programming, (Lecture Notes in Computer Science, Vol. 1381 (1998), Springer: Springer Berlin) · Zbl 0913.68025
[37] X. Li, Z. Liu, J. He, Q. Long, Generating prototypes from a UML model of requirements, in: Internat. Conf. on Distributed Computing and Internet Technology (ICDIT2004), Lecture Notes in Computer Science, Vol. 3347, Bhubaneswar, India, Springer, Berlin, 2004.; X. Li, Z. Liu, J. He, Q. Long, Generating prototypes from a UML model of requirements, in: Internat. Conf. on Distributed Computing and Internet Technology (ICDIT2004), Lecture Notes in Computer Science, Vol. 3347, Bhubaneswar, India, Springer, Berlin, 2004.
[38] Liu, Z.; He, J.; Li, X., Contract-oriented development of component systems, (Proc. of IFIP WCC-TCS2004. Proc. of IFIP WCC-TCS2004, Toulouse, France (2004), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 349-366
[39] Liu, Z.; He, J.; Li, X., rCOS: refinement of component and object systems, (in: Proc. Third Internat. Symp. on Formal Methods for Components and Objects (FMCO04), Lecture Notes in Computer Science, Vol. 3657 (2005), Springer: Springer Berlin), 222-250
[40] Liu, Z.; He, J.; Li, X.; Chen, Y., A relational model for formal requirements analysis in UML, (Dong, J. S.; Woodcock, J., Formal Methods and Software Engineering, ICFEM03, Lecture Notes in Computer Science, Vol. 2885 (2003), Springer: Springer Berlin), 641-664
[41] Liu, Z.; He, J.; Li, X.; Liu, J., Unifying views of UML, Electronic Notes Theoret. Comput. Sci. (ENTCS), 101, 95-127 (2004)
[42] Meyer, B., From structured programming to object-oriented design: the road to Eiffel, Structured Programming, 10, 1, 19-39 (1989)
[43] Mikhajlova, A.; Sekerinski, E., Class refinement and interface refinement in object-orient programs, (Proc of FME’97, Lecture Notes in Computer Science (1997), Springer: Springer Berlin)
[44] Morgan, C. C., Programming from Specifications (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0829.68083
[45] Naumann, D., Predicate transformer semantics of an Oberon-like language, (Olerog, E.-R., Proc. of PROCOMET’94 (1994), North-Holland: North-Holland Amsterdam)
[46] C. Pierik, F.S. de Boer. 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.; C. Pierik, F.S. de Boer. 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. · Zbl 1253.68087
[47] Poetzsch-Heffter, A.; Muller, P., A programming logic for sequential Java, (Swierstra, S. D., Proc. Programming Languages and Systems (ESOP’99), Lecture Notes in Computer Science, Vol. 1576 (1999), Springer: Springer Berlin), 162-176
[48] Reggio, G., Towards a rigorous semantics of UML supporting its multiview approach, (Hussmann, H., Proc. FASE 2001, Lecture Notes in Computer Science, Vol. 2029 (2001), Springer: Springer Berlin) · Zbl 0987.68864
[49] Reynolds, J., Separation logic: a logic for a shared mutable data structure, (Proc. of IEEE Symp. Logic in Computer Science (LICS’02) (2002), IEEE Computer Society: IEEE Computer Society Sliverspring, MD)
[50] D.B. Roberts, Practical Analysis for Refactoring, Ph.D. Thesis, University of Illinois, Urbana Champain, 1999.; D.B. Roberts, Practical Analysis for Refactoring, Ph.D. Thesis, University of Illinois, Urbana Champain, 1999.
[51] Sekerinski, E., A type-theoretical basis for an object-oriented refinement calculus, (Proc. of Formal Methods and Object Technology (1996), Springer: Springer Berlin)
[52] Sherif, A.; He, J.; Cavalcanti, A.; Sampaio, A., A framework for specification and validation of real-time systems using Circus actions, (in: Proc. First Internat. Colloq. on Theoretical Aspects of Computing (ICTAC04), Lecture Notes in Computer Science, Vol. 3407 (2005), Springer: Springer Berlin), 478-494 · Zbl 1108.68522
[53] Smith, G., The Object-Z Specification Language (2000), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht · Zbl 0944.68124
[54] L.A. Tokuda, Evolving Object-Oriented Designs with Refactoring, Ph.D. Thesis, University of Texas Austin, 1999.; L.A. Tokuda, Evolving Object-Oriented Designs with Refactoring, Ph.D. Thesis, University of Texas Austin, 1999.
[55] von Oheimb, D., Hoare logic for Java in Isabelle/HOL, Concurrency Comput: Practice Experience, 13, 13, 1173-1214 (2001) · Zbl 0997.68019
[56] Walker, D., \( \beta \)-calculus semantics of object-oriented programming languages, (in: Proc. TACAS’91, Lecture Notes in Computer Science, Vol. 526 (1991), Springer: Springer Berlin), 532-547 · Zbl 1493.68063
[57] Woodcock, J. C.P.; Cavalcanti, A. L.C., A semantics of Circus, (in: ZB 2002, Lecture Notes in Computer Science, Vol. 2272 (2002), Springer: Springer Berlin)
[58] Yang, J.; Long, Q.; Liu, Z.; Li, X., A predicative semantic model for integrating UML models, (in: Proc. First Internat. Colloq. on Theoretical Aspects of Computing (ICTAC04), Lecture Notes in Computer Science, Vol. 3407 (2005), Springer: Springer Berlin), 170-186 · Zbl 1108.68434
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.