Engineering of Complex Computer Systems, IEEE International Conference on (2006)
Aug. 15, 2006 to Aug. 17, 2006
Liang Zhao , United Nation University, International Institute for Software Technology, Ma
Xiangpeng Zhao , Peking University, Beijing 100871, China
Quan Long , Peking University, Beijing 100871, China
Zongyan Qiu , Peking University, Beijing 100871, China
Being a successful technique in software practice, Object Orientation (OO) is a hot topic in academic research fields. Among many formalisms, rCOS, a refinement calculus of object-oriented systems based on Unifying Theories of Programming (UTP), has been proven a promising one in the sense of its applications to incremental software constructions, the formal use of UML, etc. However, equipped with a semantics reasoning on both static and dynamic properties, rCOS is not designed for static checking. We believe introducing static checking will extend the power of rCOS. In this paper, we develop a type system for rCOS and prove some type safety theorems. To make the theoretical results of this paper convincible and easy to be understood, we follow the traditional approaches of type systems construction. That is, we use an operational semantics as the basic explanation of rCOS language in spite of the fact that rCOS is originally developed in a denotational framework.
X. Zhao, L. Zhao, Zongyan Qiu and Q. Long, "A Type System for the Relational Calculus of Object Systems," 11th IEEE International Conference on Engineering of Complex Computer Systems(ICECCS), Stanford, CA, 2006, pp. 189-198.