School of Computing

Constraint-oriented style for object-oriented formal specification

Tommaso Bolognesi and John Derrick

IEE Proceedings Software, 145(2-3):182-196, April 1998.


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

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 = {},
    ISSN = {1462-5970},
    journal = {IEE Proceedings Software},
    number = {2-3},
    publisher = {IEE},
    volume = {145},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014