Cookies on this website

We use cookies to ensure that we give you the best experience on our website. If you click 'Accept all cookies' we'll assume that you are happy to receive all cookies and you won't see this message again. If you click 'Reject all non-essential cookies' only necessary cookies providing core functionality such as security, network management, and accessibility will be enabled. Click 'Find out more' for information on how to change your cookie settings.

Many approaches to software specification and design make use of invariants: statements whose truth is preserved under various operations upon a system or component. Approaches that involve the construction of object-oriented or entity-relationship models require the expression of a particular kind of global invariant, concerning associations between objects or entities. This paper shows how association invariants can be expressed in a new, object-based formal language. It then explains how these expressions can be used to determine pre- and post-conditions for local operations, sufficient to ensure that the invariants are maintained. These conditions - and the program text to implement them - can be generated automatically. This makes it easier to produce correct implementations of an object-oriented design. © 2005 IEEE.

Original publication

DOI

10.1109/SEFM.2005.9

Type

Conference paper

Publication Date

01/12/2005

Pages

282 - 291