A Modular Theory of Object Orientation in Higher-Order UTP.
Lecture Notes in Computer Science(2014)
摘要
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.
更多查看译文
关键词
unification,semantics,models,integration,refinement
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络