Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Sept. 7, 2005 to Sept. 9, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.9
James Welch , Oxford University, UK
David Faitelson , Oxford University, UK
Jim Davies , Oxford University, UK
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.
J. Welch, J. Davies and D. Faitelson, "Automatic Maintenance of Association Invariants," Third IEEE International Conference on Software Engineering and Formal Methods(SEFM), Koblenz, 2005, pp. 282-292.