© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Constraint-oriented style for object-oriented formal specification
Tommaso Bolognesi and John Derrick
IEE Proceedings Software, 145(2-3):182-196, April 1998.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.
Download publication 294 kbytes (PostScript)Bibtex Record
@article{612,
author = {Tommaso Bolognesi and John Derrick},
title = {Constraint-oriented style for object-oriented formal specification},
month = {April},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/612},
ISSN = {1462-5970},
journal = {IEE Proceedings Software},
number = {2-3},
publisher = {IEE},
volume = {145},
}