A Modular Theory of Object Orientation in Higher-Order UTP

Frank Zeyda, Thiago Santos, Ana Cavalcanti, Augusto Sampaio

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Abstract

    Hoare and He’s Unifying Theories of Programming (UTP) is a framework that facilitates the integration of relational theories. None of the UTP theories of object orientation, however, supports recursion, dynamic binding, and compositional method definitions all at the same time. In addition, most of them are defined for a fixed language and do not lend themselves easily for integration with other UTP theories. Here, we present a novel theory of object orientation in the UTP that supports all of the aforementioned features while permitting its integration with other UTP theories. Our new theory also provides novel insights into how higher-order programming can be used to reason about object-oriented programs in a compositional manner. We exemplify its use by creating an object-oriented variant of a refinement language for real-time systems.
    Original languageEnglish
    Title of host publicationFM 2014: Formal Methods
    PublisherSpringer
    Pages627-642
    Volume8442
    ISBN (Electronic)978-3-319-06410-9
    ISBN (Print)978-3-319-06409-3
    DOIs
    Publication statusPublished - 10 May 2014
    EventFM 2014: Formal Methods 19th International Symposium - , Singapore
    Duration: 12 May 201416 May 2014

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743

    Conference

    ConferenceFM 2014: Formal Methods 19th International Symposium
    CountrySingapore
    Period12/05/1416/05/14

    Fingerprint Dive into the research topics of 'A Modular Theory of Object Orientation in Higher-Order UTP'. Together they form a unique fingerprint.

  • Cite this

    Zeyda, F., Santos, T., Cavalcanti, A., & Sampaio, A. (2014). A Modular Theory of Object Orientation in Higher-Order UTP. In FM 2014: Formal Methods (Vol. 8442, pp. 627-642). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-319-06410-9_42