rCOS: A refinement calculus of object systems

He Jifeng; Xiaoshan Li; Zhiming Liu

doi:10.1016/j.tcs.2006.07.034

rCOS: A refinement calculus of object systems

He Jifeng
, Xiaoshan Li
, Zhiming Liu^*

^*Corresponding author for this work

Software Engineering Institute

Research output: Contribution to journal › Article › peer-review

89 Scopus citations

Abstract

This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioural refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He's Unifying Theories of Programming (UTP).

Original language	English
Pages (from-to)	109-142
Number of pages	34
Journal	Theoretical Computer Science
Volume	365
Issue number	1-2
DOIs	https://doi.org/10.1016/j.tcs.2006.07.034
State	Published - 10 Nov 2006

Keywords

Object orientation
Refinement
Semantics
UTP

Access to Document

10.1016/j.tcs.2006.07.034

Cite this

@article{f7405dfe3e4c4262a977bda1386dfb28,

title = "rCOS: A refinement calculus of object systems",

abstract = "This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioural refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He's Unifying Theories of Programming (UTP).",

keywords = "Object orientation, Refinement, Semantics, UTP",

author = "He Jifeng and Xiaoshan Li and Zhiming Liu",

year = "2006",

month = nov,

day = "10",

doi = "10.1016/j.tcs.2006.07.034",

language = "英语",

volume = "365",

pages = "109--142",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

number = "1-2",

}

TY - JOUR

T1 - rCOS

T2 - A refinement calculus of object systems

AU - Jifeng, He

AU - Li, Xiaoshan

AU - Liu, Zhiming

PY - 2006/11/10

Y1 - 2006/11/10

N2 - This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioural refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He's Unifying Theories of Programming (UTP).

AB - This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioural refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He's Unifying Theories of Programming (UTP).

KW - Object orientation

KW - Refinement

KW - Semantics

KW - UTP

UR - https://www.scopus.com/pages/publications/33750045490

U2 - 10.1016/j.tcs.2006.07.034

DO - 10.1016/j.tcs.2006.07.034

M3 - 文章

AN - SCOPUS:33750045490

SN - 0304-3975

VL - 365

SP - 109

EP - 142

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1-2

ER -

rCOS: A refinement calculus of object systems

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this