zbMATH — the first resource for mathematics

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).

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
Full Text: DOI
[1] Abadi, M.; Leino, R., A logic of object-oriented programs, (), 682-696
[2] Abraham-Mumm, E.; de Boer, F.S.; de Roever, W.P.; Steffen, M., Verification for Java’s reentrant multithreading concept, (), 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.
[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 Berlin
[7] Back, R.J.R.; Petre, L.; Paltor, I.P., Formalizing UML use cases in the refinement calculus, ()
[8] Bonsangue, M.M.; Kok, J.N.; Sere, K., An approach to object-orientation in action systems, (), 68-95
[9] Booch, G.; Rumbaugh, J.; Jacobson, I., The unified modelling language user guide, (1999), Addison-Wesley Berlin, MA
[10] Borba, P.; Sampaio, A.; Cornélio, M., A refinment algebra for object-oriented programming, (), 457-482
[11] Broy, M., Object-oriented programming and software development—a critical assessment, ()
[12] Bruce, K.; Grabtre, J.; Kanapathy, G., An operational semantics for TOOPLE: a statically-typed object-oriented programming language, (), 603-626
[13] Cavalcanti, A.; Naumann, D., A weakest precondition semantics for an object-oriented language of refinement, (), 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. · Zbl 1235.68050
[15] Coleman, D., Object-oriented development: the FUSION method, (1994), Prentice-Hall Englewood cliffs, NJ
[16] Cook, S.; Daniels, J., Designing object systems: object-oriented modelling with syntropy, (1994), Prentice-Hall Englewood Cliffs, NJ · Zbl 0841.68029
[17] Dürr, E.; Dusink, E.M., The role of \(\mathit{VDM}^{++}\) in the development of a real-time tracking and tracing system, ()
[18] Fowler, M.; Beck, K.; Brant, J.; Opdyke, W.; Roberts, D., Refactoring: improving the design of existing code, (1999), Addison-Wesley Reading, MA
[19] Fowler, M., Refectoring improving the design of existing code, (2000), Addison-Wesley Reading, MA
[20] Gamma, E.; Helm, R.; Johnson, R.; Vlissides, J., Design patterns, elements of reusable object-oriented software, (1994), Addison-Wesley Reading, MA
[21] Gamma, E., Design patterns, (1995), 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.
[23] He, J.; Li, X.; Liu, Z., Component-based software engineering, (), 70-95 · Zbl 1169.68366
[24] He, J.; Liu, Z.; Li, X., Towards a refinement calculus for object-oriented systems (invited talk), ()
[25] 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. · 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 Englewood Cliffs, NJ · Zbl 1005.68036
[29] 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, (), 284-303
[31] Jacobson, I.; Booch, G.; Rumbaugh, J., The unified software development process, (1999), Addison-Wesley Reading, MA
[32] Jin, N.; He, J., Resource models and pre-compiler specification for hardware/software, (), 28-30
[33] Kruchten, P., The rational unified process—an introduction, (2000), Addison-Wesly Reading, MA
[34] Lano, K.; Haughton, H., Object-oriented specification case studies, (1994), Prentice-Hall New York · Zbl 0827.68072
[35] Larman, C., Applying UML and patterns, (2001), Prentice-Hall International Englewood Cliffs, NJ
[36] Leino, K.R.M., Recursive object types in a logic of object-oriented programming, () · 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.
[38] Liu, Z.; He, J.; Li, X., Contract-oriented development of component systems, (), 349-366
[39] Liu, Z.; He, J.; Li, X., Rcos: refinement of component and object systems, (), 222-250
[40] Liu, Z.; He, J.; Li, X.; Chen, Y., A relational model for formal requirements analysis in UML, (), 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, ()
[44] Morgan, C.C., Programming from specifications, (1994), Prentice-Hall Englewood Cliffs, NJ · Zbl 0829.68083
[45] Naumann, D., Predicate transformer semantics of an oberon-like language, ()
[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. · Zbl 1253.68087
[47] Poetzsch-Heffter, A.; Muller, P., A programming logic for sequential Java, (), 162-176
[48] Reggio, G., Towards a rigorous semantics of UML supporting its multiview approach, () · Zbl 0987.68864
[49] Reynolds, J., Separation logic: a logic for a shared mutable data structure, ()
[50] 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, ()
[52] Sherif, A.; He, J.; Cavalcanti, A.; Sampaio, A., A framework for specification and validation of real-time systems using circus actions, (), 478-494 · Zbl 1108.68522
[53] Smith, G., The object-Z specification language, (2000), 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.
[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, (), 532-547
[57] Woodcock, J.C.P.; Cavalcanti, A.L.C., A semantics of circus, ()
[58] Yang, J.; Long, Q.; Liu, Z.; Li, X., A predicative semantic model for integrating UML models, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.