The Community for Technology Leaders
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Koblenz, Germany
Sept. 7, 2005 to Sept. 9, 2005
ISBN: 0-7695-2435-4
pp: 282-292
James Welch , Oxford University, UK
Jim Davies , Oxford University, UK
David Faitelson , Oxford University, UK
ABSTRACT
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 objectoriented design.
INDEX TERMS
null
CITATION
James Welch, Jim Davies, David Faitelson, "Automatic Maintenance of Association Invariants", Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), vol. 00, no. , pp. 282-292, 2005, doi:10.1109/SEFM.2005.9
88 ms
(Ver 3.3 (11022016))