rCOS : A Refinement Calculus of Internetware Systems
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 castin
- PDF / 764,598 Bytes
- 33 Pages / 504.567 x 720 pts Page_size
- 88 Downloads / 170 Views
14
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 behavioral 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
14.1 Introduction Software engineering is mainly concerned with using techniques to systematically develop large and complex program suites. In the search for techniques for making software development more productive and software systems more reliable, objectoriented programming and formal methods are two important but largely independent
Parts of this chapter were reprinted from Jifeng He, Xiaoshan Li and Zhiming Liu. rCOS: A refinement calculus of object systems. Theoretical Computer Science, Vol. 365, Issues 1–2, pp. 109–142. © 2006 ACM, Inc. http://doi.acm.org/10.1016/j.tcs.2006.07.034.
approaches which have been influential in recent years. The concept of objects is important concept in software development. Experimental languages of the 1970s provided various definitions of package, cluster, module, etc. They promote modularity and encapsulation, allowing the construction of software components which hide state representations and algorithmic mechanisms from users, and export only pertinent features. This produces components with a level of abstraction by separating the view of what a module does from the details of how it does them. It is clear that certain features of objects, particularly inheritance and the use of object references as part of the data stored by an object, could be used to construct large system incrementally and efficiently, as wellas making it
© Springer Science+Business Media Singapore 2016 H. Mei and J. Lü, Internetware, DOI 10.1007/978-981-10-2546-4_14
301
302
possible to reuse objects in different contexts. It is essential that software engineering is given the same basis in mathematics as other engineering disciplines. There has been good progress, resulting in three main paradigms: model-based, algebraic and process calculi. Practitioners of formal methods and experts in object technology have investigated how formal specification can supplement object-oriented development [1], and how it may help to clarify the semantics of objectoriented notations and concepts. Examples of such work include the formalization of the OMG’s core object model [1] using Z. Model-based formalisms have been used extensively in conjunction with object-oriented techniques, via languages such as Object-Z [1], VDM++ [2], and methods such as Syntropy [3] which uses the Z notation and Fusion [4] that is based on VDM. Whilst these formalisms are effec
Data Loading...
