A Modular Theory of Object Orientation in Higher-Order UTP

Frank Zeyda; Thiago Santos; Ana Cavalcanti; Augusto Sampaio

doi:10.1007/978-3-319-06410-9_42

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 proceeding › Conference 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 language	English
Title of host publication	FM 2014: Formal Methods
Publisher	Springer
Pages	627-642
Volume	8442
ISBN (Electronic)	978-3-319-06410-9
ISBN (Print)	978-3-319-06409-3
DOIs	https://doi.org/10.1007/978-3-319-06410-9_42
Publication status	Published - 10 May 2014
Event	FM 2014: Formal Methods 19th International Symposium - , Singapore Duration: 12 May 2014 → 16 May 2014

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
ISSN (Print)	0302-9743

Conference

Conference	FM 2014: Formal Methods 19th International Symposium
Country/Territory	Singapore
Period	12/05/14 → 16/05/14

Access to Document

10.1007/978-3-319-06410-9_42Licence: Other

Cite this

@inproceedings{8109f2621c204c17b2ccb21fe49910ce,

title = "A Modular Theory of Object Orientation in Higher-Order UTP",

abstract = "Hoare and He{\textquoteright}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.",

author = "Frank Zeyda and Thiago Santos and Ana Cavalcanti and Augusto Sampaio",

year = "2014",

month = may,

day = "10",

doi = "10.1007/978-3-319-06410-9_42",

language = "English",

isbn = "978-3-319-06409-3",

volume = "8442",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "627--642",

booktitle = "FM 2014: Formal Methods",

note = "FM 2014: Formal Methods 19th International Symposium ; Conference date: 12-05-2014 Through 16-05-2014",

}

TY - GEN

T1 - A Modular Theory of Object Orientation in Higher-Order UTP

AU - Zeyda, Frank

AU - Santos, Thiago

AU - Cavalcanti, Ana

AU - Sampaio, Augusto

PY - 2014/5/10

Y1 - 2014/5/10

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

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

U2 - 10.1007/978-3-319-06410-9_42

DO - 10.1007/978-3-319-06410-9_42

M3 - Conference contribution

SN - 978-3-319-06409-3

VL - 8442

T3 - Lecture Notes in Computer Science

SP - 627

EP - 642

BT - FM 2014: Formal Methods

PB - Springer

T2 - FM 2014: Formal Methods 19th International Symposium

Y2 - 12 May 2014 through 16 May 2014

ER -

A Modular Theory of Object Orientation in Higher-Order UTP

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this