Paper Info
Title
A Type System for the Relational Calculus of Object Systems
Abstract
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.
Year
DOI
Venue
2006
10.1109/ICECCS.2006.47
ICECCS
Keywords
Field
DocType
type system,refinement calculus,type safety,object oriented programming,object oriented,relational algebra,type theory,operational semantics
Relational calculus,Operational semantics,Programming language,Object-oriented programming,Unified Modeling Language,Refinement calculus,Computer science,Type theory,Type safety,Rotation formalisms in three dimensions
Conference
Volume
Issue
ISBN
null
null
0-7695-2530-X
Citations 
PageRank 
References 
3
0.44
10
Authors
4
Name
Order
Citations
PageRank
Liang Zhao110013.74
Xiangpeng Zhao235320.67
Quan Long3645.63
Zongyan Qiu443641.04