Constraint-oriented style for object-oriented formal specification

Bolognesi, T. and Derrick, J. (1998) Constraint-oriented style for object-oriented formal specification. IEE Proceedings Software, 145 (2-3). pp. 61-69. ISSN 1462-5970. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)

Abstract

We propose a specification style which combines the features and advantages of object-oriented and constraint-oriented system decomposition. A system description is decomposed into data-handling objects, which usually reflect objects and individual operations in the real system, and temporal-ordering constraints, which capture aspects of functionality as behavioural sequences, with a possibility to introduce also entities which blurr the distinction between these two extreme cases. Composition is achieved via synchronisation on shared operations: different objects/constraints insisting on an operation express different views on the enabling conditions and effects of that operation. Objects, constraints, and their composition can be formally specified in Object-Z, an object-oriented extension of the Z notation, with pure temporal ordering constraints equivalently expressed as transition graphs. However, expressing object/constraint compositions in Object-Z is cumbersome. We solve this problem by proposing a natural textual notation, called co-expression, which is a most direct description of an object/constraint interconnection graph, and we define a mapping from co-expressions to Object-Z. Thus, specifications in an object/constraint-oriented style can be conveniently written using transition graphs and interconnection diagrams mixed with Object-Z text, and then translated into this language.

Item Type: Article
Uncontrolled keywords: Object-oriented, Formal specification, constraint-oriented style, Object-Z
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 22 Aug 2009 00:22
Last Modified: 12 Jun 2012 14:00
Resource URI: http://kar.kent.ac.uk/id/eprint/21669 (The current URI for this page, for reference purposes)
  • Depositors only (login required):